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: ( ( 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 A2: ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 ) ; :: thesis: Sum Fn = 0

now

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

end;

hence Sum Fn = 0 ; :: thesis: verum

end;

( 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 A3: 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 A4: len Fn > 0 ; :: thesis: ( len Fn = 0 or for n being Element of NAT st n in dom Fn holds
Fn . n = 0 )

assume ( not len Fn = 0 & ex n being Element of NAT st
( n in dom Fn & not Fn . n = 0 ) ) ; :: thesis: contradiction
then consider n being Element of NAT such that
A5: ( n in dom Fn & Fn . n <> 0 ) ;
Sum Fn >= Fn . n by A4, A5, Th52;
hence contradiction by A3, A5; :: 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;

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