let F be Function of NAT , ExtREAL ; :: thesis: ( ( for n being Element of NAT holds F . n = 0. ) implies SUM F = 0. )
assume A1: for n being Element of NAT holds F . n = 0. ; :: thesis: SUM F = 0.
defpred S₁[ Element of NAT ] means (Ser F) . $1 = 0. ;
A2: (Ser F) . 0 = F . 0 by SUPINF_2:63
.= 0. by A1 ;
then A3: S₁[ 0 ] ;
A4: for t being Element of NAT st S₁[t] holds
S₁[t + 1]

proof

let t be Element of NAT ; :: thesis: ( S₁[t] implies S₁[t + 1] )
assume (Ser F) . t = 0. ; :: thesis: S₁[t + 1]
hence (Ser F) . (t + 1) = 0. + (F . (t + 1)) by SUPINF_2:63
.= F . (t + 1) by SUPINF_2:18
.= 0. by A1 ;
:: thesis: verum

end;

A5: for s being Element of NAT holds S₁[s] from NAT_1:sch 1(A3, A4);
A6: sup {0. } = 0. by XXREAL_2:11;
rng (Ser F) = {0. }

proof

A7: ( dom (Ser F) = NAT & rng (Ser F) c= ExtREAL ) by FUNCT_2:def 1;
thus rng (Ser F) c= {0. } :: according to XBOOLE_0:def 10 :: thesis: {0. } c= rng (Ser F)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (Ser F) or x in {0. } )
assume x in rng (Ser F) ; :: thesis: x in {0. }
then consider s being set such that
A8: ( s in dom (Ser F) & x = (Ser F) . s ) by FUNCT_1:def 5;
reconsider s = s as Element of NAT by A8;
(Ser F) . s = 0. by A5;
hence x in {0. } by A8, TARSKI:def 1; :: thesis: verum

end;

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in {0. } or x in rng (Ser F) )
assume x in {0. } ; :: thesis: x in rng (Ser F)
then x = 0. by TARSKI:def 1;
hence x in rng (Ser F) by A2, A7, FUNCT_1:def 5; :: thesis: verum

end;

hence SUM F = 0. by A6, SUPINF_2:def 23; :: thesis: verum