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) \/ () 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 ;
then not -infty in {x} by FINSEQ_1:38;
then A6: x <> -infty by TARSKI:def 1;
A7: Sum F <> -infty by ;
F ^ (H ^ <*x*>) = (F ^ H) ^ <*x*> by FINSEQ_1:32;
hence Sum (F ^ (H ^ <*x*>)) = ((Sum F) + (Sum H)) + x by
.= (Sum F) + ((Sum H) + x) by
.= (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 () ; :: thesis: Sum (F ^ ()) = (Sum F) + ()
thus Sum (F ^ ()) = Sum F by FINSEQ_1:34
.= (Sum F) + () by ; :: thesis: verum
end;
for H being FinSequence of ExtREAL holds S1[H] from hence Sum (F ^ G) = (Sum F) + (Sum G) by A8; :: thesis: verum