defpred S₁[ FinSequence of ExtREAL ] means ( rng $1 c= {0. } implies Sum $1 = 0. );
A1: S₁[ <*> ExtREAL ] by Th4;
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:44;
then rng <*x*> c= {0. } by XBOOLE_1:11;
then {x} c= {0. } by FINSEQ_1:55;
then x in {0. } by ZFMISC_1:37;
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: for F being FinSequence of ExtREAL holds S₁[F] from FINSEQ_2:sch 2(A1, A2);
let F be FinSequence of ExtREAL ; :: thesis: ( rng F c= {0. } implies Sum F = 0. )
assume rng F c= {0. } ; :: thesis: Sum F = 0.
hence Sum F = 0. by A6; :: thesis: verum