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

end;

thus for F being FinSequence of ExtREAL holds S₁[F] from FINSEQ_2:sch 2(A1, A2); :: thesis: verum