let Fn be XFinSequence of NAT ; :: thesis: ( Sum Fn = 0 iff ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) )
A1: ( not Sum Fn = 0 or len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 )

proof

assume A2: Sum Fn = 0 ; :: thesis: ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 )

now

per cases ( len Fn = 0 or len Fn > 0 ) ;

suppose len Fn = 0 ; :: thesis: ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 )

hence ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) ; :: thesis: verum

end;

suppose A3: len Fn > 0 ; :: thesis: ( not len Fn = 0 implies for n being Element of NAT st n in dom Fn holds
Fn . n = 0 )

assume that
not len Fn = 0 and
A4: ex n being Element of NAT st
( n in dom Fn & not Fn . n = 0 ) ; :: thesis: contradiction
thus contradiction by A2, A3, A4, Th52; :: thesis: verum

end;

end;

end;

hence ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) ; :: thesis: verum

end;

( ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) implies Sum Fn = 0 )

proof

assume ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) ; :: thesis: Sum Fn = 0
then for n being Element of NAT st n in dom Fn holds
Fn . n <= 0 ;
then Sum Fn <= (len Fn) * 0 by Th50;
hence Sum Fn = 0 ; :: thesis: verum

end;

hence ( Sum Fn = 0 iff ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) ) by A1; :: thesis: verum