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

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

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

A1: for F being FinSequence of ExtREAL

for x being Element of ExtREAL st S

S

proof

A5:
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*>]

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;S

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

assume A2: S

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

thus for F being FinSequence of ExtREAL holds S