theorem :: NUMERAL3:73

for b being non zero Nat
for f being XFinSequence of NAT st value (f,b) = 0 holds
f is empty-yielding