let b be non zero Nat; :: thesis: for f being XFinSequence of NAT st value (f,b) = 0 holds
f is empty-yielding
let f be XFinSequence of NAT ; :: thesis: ( value (f,b) = 0 implies f is empty-yielding )
assume A1: value (f,b) = 0 ; :: thesis: f is empty-yielding
consider x being XFinSequence of NAT such that
A2: ( dom x = dom f & ( for i being Nat st i in dom x holds
x . i = (f . i) * (b |^ i) ) & value (f,b) = Sum x ) by NUMERAL1:def 1;
for k being Nat st k in dom x holds
f . k = 0

proof

assume ex k being Nat st
( k in dom x & not f . k = 0 ) ; :: thesis: contradiction
then consider k being Nat such that
B1: ( k in dom x & f . k <> 0 ) ;
B2: x . k = (f . k) * (b |^ k) by A2, B1;
reconsider x = x as natural-valued XFinSequence ;
Sum x >= x . k by NAT_1:3, AFINSQ_2:61, B1;
hence contradiction by A1, A2, B2, B1; :: thesis: verum

end;

hence f is empty-yielding by A2; :: thesis: verum