defpred S₁[ FinSequence of ExtREAL ] means ( +infty in rng $1 & 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*>]
assume that
A3: +infty in rng (F ^ <*x*>) and
A4: not -infty in rng (F ^ <*x*>) ; :: thesis: Sum (F ^ <*x*>) = +infty
A5: Sum (F ^ <*x*>) = (Sum F) + x by Lm4;
+infty in (rng F) \/ (rng <*x*>) by A3, FINSEQ_1:31;
then ( +infty in rng F or +infty in rng <*x*> ) by XBOOLE_0:def 3;
then A6: ( +infty in rng F or +infty in {x} ) by FINSEQ_1:38;
A7: not -infty in (rng F) \/ (rng <*x*>) by A4, FINSEQ_1:31;
then not -infty in rng F by XBOOLE_0:def 3;
then A8: Sum F <> -infty by Lm5;
not -infty in rng <*x*> by A7, XBOOLE_0:def 3;
then not -infty in {x} by FINSEQ_1:38;
then A9: x <> -infty by TARSKI:def 1;

per cases ( +infty in rng F or +infty = x ) by A6, TARSKI:def 1;

suppose +infty in rng F ; :: thesis: Sum (F ^ <*x*>) = +infty

hence Sum (F ^ <*x*>) = +infty by A2, A7, A9, A5, XBOOLE_0:def 3, XXREAL_3:def 2; :: thesis: verum

end;

suppose +infty = x ; :: thesis: Sum (F ^ <*x*>) = +infty

hence Sum (F ^ <*x*>) = +infty by A5, A8, XXREAL_3:def 2; :: thesis: verum

end;

end;

end;

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