theorem Th1: :: NUMBER11:1

for b being Nat
for E being XFinSequence of NAT st E = {} holds
value (E,b) = 0