let b be Nat; :: thesis: for E being XFinSequence of NAT st E = {} holds
value (E,b) = 0
let E be XFinSequence of NAT ; :: thesis: ( E = {} implies value (E,b) = 0 )
assume A1: E = {} ; :: thesis: value (E,b) = 0
then A2: for i being Nat st i in dom E holds
E . i = (E . i) * (b |^ i) ;
Sum E = 0 by A1;
hence value (E,b) = 0 by A2, NUMERAL1:def 1; :: thesis: verum