let F be FinSequence of ExtREAL ; :: thesis: ( rng F c= {0.} implies Sum F = 0. )
defpred S₁[ FinSequence of ExtREAL ] means ( rng $1 c= {0.} implies Sum $1 = 0. );
assume A1: rng F c= {0.} ; :: thesis: Sum F = 0.
A2: for F being FinSequence of ExtREAL
for x being Element of ExtREAL st S₁[F] holds
S₁[F ^ <*x*>]

proof

let F be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S₁[F] holds
S₁[F ^ <*x*>]
let x be Element of ExtREAL ; :: thesis: ( S₁[F] implies S₁[F ^ <*x*>] )
assume A3: S₁[F] ; :: thesis: S₁[F ^ <*x*>]
assume rng (F ^ <*x*>) c= {0.} ; :: thesis: Sum (F ^ <*x*>) = 0.
then A4: (rng F) \/ (rng <*x*>) c= {0.} by FINSEQ_1:31;
then rng <*x*> c= {0.} by XBOOLE_1:11;
then {x} c= {0.} by FINSEQ_1:38;
then x in {0.} by ZFMISC_1:31;
then A5: x = 0. by TARSKI:def 1;
thus Sum (F ^ <*x*>) = (Sum F) + x by Lm4
.= 0. by A3, A4, A5, XBOOLE_1:11 ; :: thesis: verum

end;

A6: S₁[ <*> ExtREAL] by EXTREAL1:7;
for F being FinSequence of ExtREAL holds S₁[F] from FINSEQ_2:sch 2(A6, A2);
hence Sum F = 0. by A1; :: thesis: verum