let F, G, H be FinSequence of ExtREAL ; :: thesis: ( F is nonnegative & G is nonnegative & dom F = dom G & H = F + G implies Sum H = (Sum F) + (Sum G) )
assume that
A1: F is nonnegative and
A2: G is nonnegative and
A3: dom F = dom G and
A4: H = F + G ; :: thesis: Sum H = (Sum F) + (Sum G)
for y being object st y in rng F holds
not y in {-infty}
proof
let y be object ; :: thesis: ( y in rng F implies not y in {-infty} )
assume y in rng F ; :: thesis: not y in {-infty}
then consider x being object such that
A5: x in dom F and
A6: y = F . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A5;
0. <= F . x by A1, SUPINF_2:39;
hence not y in {-infty} by A6, TARSKI:def 1; :: thesis: verum
end;
then rng F misses {-infty} by XBOOLE_0:3;
then A7: F " {-infty} = {} by RELAT_1:138;
for y being object st y in rng G holds
not y in {-infty}
proof
let y be object ; :: thesis: ( y in rng G implies not y in {-infty} )
assume y in rng G ; :: thesis: not y in {-infty}
then consider x being object such that
A8: x in dom G and
A9: y = G . x by FUNCT_1:def 3;
reconsider x = x as Element of NAT by A8;
0. <= G . x by A2, SUPINF_2:39;
hence not y in {-infty} by A9, TARSKI:def 1; :: thesis: verum
end;
then rng G misses {-infty} by XBOOLE_0:3;
then A10: G " {-infty} = {} by RELAT_1:138;
A11: dom H = ((dom F) /\ (dom G)) \ (((F " {-infty}) /\ (G " {+infty})) \/ ((F " {+infty}) /\ (G " {-infty}))) by A4, MESFUNC1:def 3
.= dom F by A3, A7, A10 ;
then A12: len H = len F by FINSEQ_3:29;
consider h being sequence of ExtREAL such that
A13: Sum H = h . (len H) and
A14: h . 0 = 0. and
A15: for i being Nat st i < len H holds
h . (i + 1) = (h . i) + (H . (i + 1)) by EXTREAL1:def 2;
consider f being sequence of ExtREAL such that
A16: Sum F = f . (len F) and
A17: f . 0 = 0. and
A18: for i being Nat st i < len F holds
f . (i + 1) = (f . i) + (F . (i + 1)) by EXTREAL1:def 2;
consider g being sequence of ExtREAL such that
A19: Sum G = g . (len G) and
A20: g . 0 = 0. and
A21: for i being Nat st i < len G holds
g . (i + 1) = (g . i) + (G . (i + 1)) by EXTREAL1:def 2;
defpred S1[ Nat] means ( $1 <= len H implies h . $1 = (f . $1) + (g . $1) );
A22: len H = len G by A3, A11, FINSEQ_3:29;
A23: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A24: S1[k] ; :: thesis: S1[k + 1]
assume A25: k + 1 <= len H ; :: thesis: h . (k + 1) = (f . (k + 1)) + (g . (k + 1))
reconsider k = k as Element of NAT by ORDINAL1:def 12;
A26: k < len H by A25, NAT_1:13;
then A27: ( f . (k + 1) = (f . k) + (F . (k + 1)) & g . (k + 1) = (g . k) + (G . (k + 1)) ) by A18, A21, A12, A22;
1 <= k + 1 by NAT_1:11;
then A28: k + 1 in dom H by A25, FINSEQ_3:25;
A29: ( f . k <> -infty & g . k <> -infty & F . (k + 1) <> -infty & G . (k + 1) <> -infty )
proof
defpred S2[ Nat] means ( $1 <= len H implies g . $1 <> -infty );
defpred S3[ Nat] means ( $1 <= len H implies f . $1 <> -infty );
A30: for m being Nat st S3[m] holds
S3[m + 1]
proof
let m be Nat; :: thesis: ( S3[m] implies S3[m + 1] )
assume A31: S3[m] ; :: thesis: S3[m + 1]
assume A32: m + 1 <= len H ; :: thesis: f . (m + 1) <> -infty
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A33: 0. <= F . (m + 1) by A1, SUPINF_2:39;
m < len H by A32, NAT_1:13;
then f . (m + 1) = (f . m) + (F . (m + 1)) by A18, A12;
hence f . (m + 1) <> -infty by A31, A32, A33, NAT_1:13, XXREAL_3:17; :: thesis: verum
end;
A34: S3[ 0 ] by A17;
for i being Nat holds S3[i] from NAT_1:sch 2(A34, A30);
 hence f . k <> -infty by A26; :: thesis: ( g . k <> -infty & F . (k + 1) <> -infty & G . (k + 1) <> -infty )
A35: for m being Nat st S2[m] holds
S2[m + 1]
proof
let m be Nat; :: thesis: ( S2[m] implies S2[m + 1] )
assume A36: S2[m] ; :: thesis: S2[m + 1]
assume A37: m + 1 <= len H ; :: thesis: g . (m + 1) <> -infty
reconsider m = m as Element of NAT by ORDINAL1:def 12;
A38: 0. <= G . (m + 1) by A2, SUPINF_2:39;
m < len H by A37, NAT_1:13;
then g . (m + 1) = (g . m) + (G . (m + 1)) by A21, A22;
hence g . (m + 1) <> -infty by A36, A37, A38, NAT_1:13, XXREAL_3:17; :: thesis: verum
end;
A39: S2[ 0 ] by A20;
for i being Nat holds S2[i] from NAT_1:sch 2(A39, A35);
 hence g . k <> -infty by A26; :: thesis: ( F . (k + 1) <> -infty & G . (k + 1) <> -infty )
thus F . (k + 1) <> -infty by A1, SUPINF_2:51; :: thesis: G . (k + 1) <> -infty
thus G . (k + 1) <> -infty by A2, SUPINF_2:51; :: thesis: verum
end;
then A40: (f . k) + (F . (k + 1)) <> -infty by XXREAL_3:17;
A41: h . (k + 1) = ((f . k) + (g . k)) + (H . (k + 1)) by A15, A24, A26
.= ((f . k) + (g . k)) + ((F . (k + 1)) + (G . (k + 1))) by A4, A28, MESFUNC1:def 3 ;
(f . k) + (g . k) <> -infty by A29, XXREAL_3:17;
then h . (k + 1) = (((f . k) + (g . k)) + (F . (k + 1))) + (G . (k + 1)) by A41, A29, XXREAL_3:29
.= (((f . k) + (F . (k + 1))) + (g . k)) + (G . (k + 1)) by A29, XXREAL_3:29
.= (f . (k + 1)) + (g . (k + 1)) by A27, A29, A40, XXREAL_3:29 ;
hence h . (k + 1) = (f . (k + 1)) + (g . (k + 1)) ; :: thesis: verum
end;
A42: S1[ 0 ] by A17, A20, A14;
for i being Nat holds S1[i] from NAT_1:sch 2(A42, A23);
 hence Sum H = (Sum F) + (Sum G) by A16, A19, A13, A12, A22; :: thesis: verum