>>510
そのままだな。
完備アルキメデス順序体において「小数」を次のように定義する:

整数aと0から9までの自然数a_1, a_2, ... に対して、
0の事を「a . a_1 a_2 …」と書き、これを0の小数展開と定義する。
つまり「a . a_1 a_2 …=0」と(左辺を右辺で)定義する。

この定義の下でa . a_1 a_2 …=0が成り立つのは、正に定義そのもの。