let F be sequence of ExtREAL; :: thesis: ( ( for n being Element of NAT holds F . n = 0. ) implies SUM F = 0. )
defpred S₁[ Nat] means (Ser F) . $1 = 0. ;
assume A1: for n being Element of NAT holds F . n = 0. ; :: thesis: SUM F = 0.
A2: for t being Nat st S₁[t] holds
S₁[t + 1]

proof

let t be 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:def 11
.= F . (t + 1) by XXREAL_3:4
.= 0. by A1 ;
:: thesis: verum

end;

A3: (Ser F) . 0 = F . 0 by SUPINF_2:def 11
.= 0. by A1 ;
then A4: S₁[ 0 ] ;
A5: for s being Nat holds S₁[s] from NAT_1:sch 2(A4, A2);
A6: rng (Ser F) = {0.}

proof

thus rng (Ser F) c= {0.} :: according to XBOOLE_0:def 10 :: thesis: {0.} c= rng (Ser F)

proof

let x be object ; :: 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 object such that
A7: s in dom (Ser F) and
A8: x = (Ser F) . s by FUNCT_1:def 3;
reconsider s = s as Element of NAT by A7;
(Ser F) . s = 0. by A5;
hence x in {0.} by A8, TARSKI:def 1; :: thesis: verum

end;

let x be object ; :: 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 ( dom (Ser F) = NAT & x = 0. ) by FUNCT_2:def 1, TARSKI:def 1;
hence x in rng (Ser F) by A3, FUNCT_1:def 3; :: thesis: verum

end;

sup {0.} = 0. by XXREAL_2:11;
hence SUM F = 0. by A6; :: thesis: verum