let F, G be FinSequence of ExtREAL ; :: thesis: ( not -infty in rng F & not -infty in rng G implies Sum (F ^ G) = (Sum F) + (Sum G) )

defpred S_{1}[ FinSequence of ExtREAL ] means ( not -infty in rng $1 implies Sum (F ^ $1) = (Sum F) + (Sum $1) );

assume A1: not -infty in rng F ; :: thesis: ( -infty in rng G or Sum (F ^ G) = (Sum F) + (Sum G) )

A2: for H being FinSequence of ExtREAL

for x being Element of ExtREAL st S_{1}[H] holds

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

A9: S_{1}[ <*> ExtREAL]
_{1}[H]
from FINSEQ_2:sch 2(A9, A2);

hence Sum (F ^ G) = (Sum F) + (Sum G) by A8; :: thesis: verum

defpred S

assume A1: not -infty in rng F ; :: thesis: ( -infty in rng G or Sum (F ^ G) = (Sum F) + (Sum G) )

A2: for H being FinSequence of ExtREAL

for x being Element of ExtREAL st S

S

proof

assume A8:
not -infty in rng G
; :: thesis: Sum (F ^ G) = (Sum F) + (Sum G)
let H be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S_{1}[H] holds

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

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

assume A3: S_{1}[H]
; :: thesis: S_{1}[H ^ <*x*>]

thus S_{1}[H ^ <*x*>]
:: thesis: verum

end;S

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

assume A3: S

thus S

proof

assume
not -infty in rng (H ^ <*x*>)
; :: thesis: Sum (F ^ (H ^ <*x*>)) = (Sum F) + (Sum (H ^ <*x*>))

then A4: not -infty in (rng H) \/ (rng <*x*>) by FINSEQ_1:31;

then not -infty in rng H by XBOOLE_0:def 3;

then A5: Sum H <> -infty by Lm2;

not -infty in rng <*x*> by A4, XBOOLE_0:def 3;

then not -infty in {x} by FINSEQ_1:38;

then A6: x <> -infty by TARSKI:def 1;

A7: Sum F <> -infty by A1, Lm2;

F ^ (H ^ <*x*>) = (F ^ H) ^ <*x*> by FINSEQ_1:32;

hence Sum (F ^ (H ^ <*x*>)) = ((Sum F) + (Sum H)) + x by A3, A4, Lm1, XBOOLE_0:def 3

.= (Sum F) + ((Sum H) + x) by A6, A7, A5, XXREAL_3:29

.= (Sum F) + (Sum (H ^ <*x*>)) by Lm1 ;

:: thesis: verum

end;then A4: not -infty in (rng H) \/ (rng <*x*>) by FINSEQ_1:31;

then not -infty in rng H by XBOOLE_0:def 3;

then A5: Sum H <> -infty by Lm2;

not -infty in rng <*x*> by A4, XBOOLE_0:def 3;

then not -infty in {x} by FINSEQ_1:38;

then A6: x <> -infty by TARSKI:def 1;

A7: Sum F <> -infty by A1, Lm2;

F ^ (H ^ <*x*>) = (F ^ H) ^ <*x*> by FINSEQ_1:32;

hence Sum (F ^ (H ^ <*x*>)) = ((Sum F) + (Sum H)) + x by A3, A4, Lm1, XBOOLE_0:def 3

.= (Sum F) + ((Sum H) + x) by A6, A7, A5, XXREAL_3:29

.= (Sum F) + (Sum (H ^ <*x*>)) by Lm1 ;

:: thesis: verum

A9: S

proof

for H being FinSequence of ExtREAL holds S
set H = <*> ExtREAL;

assume not -infty in rng (<*> ExtREAL) ; :: thesis: Sum (F ^ (<*> ExtREAL)) = (Sum F) + (Sum (<*> ExtREAL))

thus Sum (F ^ (<*> ExtREAL)) = Sum F by FINSEQ_1:34

.= (Sum F) + (Sum (<*> ExtREAL)) by Th5, XXREAL_3:4 ; :: thesis: verum

end;assume not -infty in rng (<*> ExtREAL) ; :: thesis: Sum (F ^ (<*> ExtREAL)) = (Sum F) + (Sum (<*> ExtREAL))

thus Sum (F ^ (<*> ExtREAL)) = Sum F by FINSEQ_1:34

.= (Sum F) + (Sum (<*> ExtREAL)) by Th5, XXREAL_3:4 ; :: thesis: verum

hence Sum (F ^ G) = (Sum F) + (Sum G) by A8; :: thesis: verum