:: deftheorem Def1 defines value NUMERAL1:def 1 :
for d being XFinSequence of NAT
for b, b₃ being Nat holds
( b₃ = value (d,b) iff ex d9 being XFinSequence of NAT st
( dom d9 = dom d & ( for i being Nat st i in dom d9 holds
d9 . i = (d . i) * (b |^ i) ) & b₃ = Sum d9 ) );