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₁[ 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₁[H] holds
S₁[H ^ <*x*>]

proof

let H be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S₁[H] holds
S₁[H ^ <*x*>]
let x be Element of ExtREAL ; :: thesis: ( S₁[H] implies S₁[H ^ <*x*>] )
assume A3: S₁[H] ; :: thesis: S₁[H ^ <*x*>]
thus S₁[H ^ <*x*>] :: thesis: verum

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;

end;

assume A8: not -infty in rng G ; :: thesis: Sum (F ^ G) = (Sum F) + (Sum G)
A9: S₁[ <*> ExtREAL]

proof

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;

for H being FinSequence of ExtREAL holds S₁[H] from FINSEQ_2:sch 2(A9, A2);
hence Sum (F ^ G) = (Sum F) + (Sum G) by A8; :: thesis: verum