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
proof
let y be object ; :: thesis: ( y in rng F implies not y in )
assume y in rng F ; :: thesis: not y in
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 ;
hence not y in by ; :: thesis: verum
end;
then rng F misses by XBOOLE_0:3;
then A7: F " = {} by RELAT_1:138;
for y being object st y in rng G holds
not y in
proof
let y be object ; :: thesis: ( y in rng G implies not y in )
assume y in rng G ; :: thesis: not y in
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 ;
hence not y in by ; :: thesis: verum
end;
then rng G misses by XBOOLE_0:3;
then A10: G " = {} by RELAT_1:138;
A11: dom H = ((dom F) /\ (dom G)) \ ((() /\ ()) \/ (() /\ ())) by
.= 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 ;
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 ;
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 ;
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 ;
m < len H by ;
then f . (m + 1) = (f . m) + (F . (m + 1)) by ;
hence f . (m + 1) <> -infty by ; :: thesis: verum
end;
A34: S3[ 0 ] by A17;
for i being Nat holds S3[i] from 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 ;
m < len H by ;
then g . (m + 1) = (g . m) + (G . (m + 1)) by ;
hence g . (m + 1) <> -infty by ; :: thesis: verum
end;
A39: S2[ 0 ] by A20;
for i being Nat holds S2[i] from hence g . k <> -infty by A26; :: thesis: ( F . (k + 1) <> -infty & G . (k + 1) <> -infty )
thus F . (k + 1) <> -infty by ; :: thesis: G . (k + 1) <> -infty
thus G . (k + 1) <> -infty by ; :: 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
.= ((f . k) + (g . k)) + ((F . (k + 1)) + (G . (k + 1))) by ;
(f . k) + (g . k) <> -infty by ;
then h . (k + 1) = (((f . k) + (g . k)) + (F . (k + 1))) + (G . (k + 1)) by
.= (((f . k) + (F . (k + 1))) + (g . k)) + (G . (k + 1)) by
.= (f . (k + 1)) + (g . (k + 1)) by ;
hence h . (k + 1) = (f . (k + 1)) + (g . (k + 1)) ; :: thesis: verum
end;
A42: S1[ 0 ] by ;
for i being Nat holds S1[i] from hence Sum H = (Sum F) + (Sum G) by A16, A19, A13, A12, A22; :: thesis: verum