defpred S₁[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies Sum $1 <> -infty );
A1: 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 A2: S₁[F] ; :: thesis: S₁[F ^ <*x*>]
A3: Sum (F ^ <*x*>) = (Sum F) + x by Lm1;
assume not -infty in rng (F ^ <*x*>) ; :: thesis: Sum (F ^ <*x*>) <> -infty
then A4: not -infty in (rng F) \/ (rng <*x*>) by FINSEQ_1:31;
then not -infty in rng <*x*> by XBOOLE_0:def 3;
then not -infty in {x} by FINSEQ_1:38;
then x <> -infty by TARSKI:def 1;
hence Sum (F ^ <*x*>) <> -infty by A2, A4, A3, XBOOLE_0:def 3, XXREAL_3:17; :: thesis: verum

end;

A5: S₁[ <*> ExtREAL] by Th5;
thus for F being FinSequence of ExtREAL holds S₁[F] from FINSEQ_2:sch 2(A5, A1); :: thesis: verum