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 S1[ 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 S1[H] holds
S1[H ^ <*x*>]
proof
let H be FinSequence of ExtREAL ; :: thesis: for x being Element of ExtREAL st S1[H] holds
S1[H ^ <*x*>]
let x be Element of ExtREAL ; :: thesis: ( S1[H] implies S1[H ^ <*x*>] )
assume A3: S1[H] ; :: thesis: S1[H ^ <*x*>]
thus S1[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: S1[ <*> 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 S1[H] from FINSEQ_2:sch 2(A9, A2);
 hence Sum (F ^ G) = (Sum F) + (Sum G) by A8; :: thesis: verum