defpred S_{1}[ 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_{1}[F] holds

S_{1}[F ^ <*x*>]
_{1}[ <*> ExtREAL]
;

thus for F being FinSequence of ExtREAL holds S_{1}[F]
from FINSEQ_2:sch 2(A10, A1); :: thesis: verum

A1: for F being FinSequence of ExtREAL

for x being Element of ExtREAL st S

S

proof

A10:
S
let F be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S_{1}[F] holds

S_{1}[F ^ <*x*>]

let x be Element of ExtREAL ; :: thesis: ( S_{1}[F] implies S_{1}[F ^ <*x*>] )

assume A2: S_{1}[F]
; :: thesis: S_{1}[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;

end;S

let x be Element of ExtREAL ; :: thesis: ( S

assume A2: S

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;

thus for F being FinSequence of ExtREAL holds S