:: deftheorem Def2 defines digits NUMERAL1:def 2 :
for n, b being Nat st b > 1 holds
for b₃ being XFinSequence of NAT holds
( ( n <> 0 implies ( b₃ = digits (n,b) iff ( value (b₃,b) = n & b₃ . ((len b₃) - 1) <> 0 & ( for i being Nat st i in dom b₃ holds
( 0 <= b₃ . i & b₃ . i < b ) ) ) ) ) & ( not n <> 0 implies ( b₃ = digits (n,b) iff b₃ = <%0%> ) ) );