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}

then A7: F " {-infty} = {} by RELAT_1:138;

for y being object st y in rng G holds

not y in {-infty}

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 S_{1}[ 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 S_{1}[k] holds

S_{1}[k + 1]
_{1}[ 0 ]
by A17, A20, A14;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A42, A23);

hence Sum H = (Sum F) + (Sum G) by A16, A19, A13, A12, A22; :: thesis: verum

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

then
rng F misses {-infty}
by XBOOLE_0:3;
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;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

then A7: F " {-infty} = {} by RELAT_1:138;

for y being object st y in rng G holds

not y in {-infty}

proof

then
rng G misses {-infty}
by XBOOLE_0:3;
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;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

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 S

A22: len H = len G by A3, A11, FINSEQ_3:29;

A23: for k being Nat st S

S

proof

A42:
S
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A24: S_{1}[k]
; :: thesis: S_{1}[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 )

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;assume A24: S

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

then A40:
(f . k) + (F . (k + 1)) <> -infty
by XXREAL_3:17;
defpred S_{2}[ Nat] means ( $1 <= len H implies g . $1 <> -infty );

defpred S_{3}[ Nat] means ( $1 <= len H implies f . $1 <> -infty );

A30: for m being Nat st S_{3}[m] holds

S_{3}[m + 1]
_{3}[ 0 ]
by A17;

for i being Nat holds S_{3}[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 S_{2}[m] holds

S_{2}[m + 1]
_{2}[ 0 ]
by A20;

for i being Nat holds S_{2}[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;defpred S

A30: for m being Nat st S

S

proof

A34:
S
let m be Nat; :: thesis: ( S_{3}[m] implies S_{3}[m + 1] )

assume A31: S_{3}[m]
; :: thesis: S_{3}[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;assume A31: S

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

for i being Nat holds S

hence f . k <> -infty by A26; :: thesis: ( g . k <> -infty & F . (k + 1) <> -infty & G . (k + 1) <> -infty )

A35: for m being Nat st S

S

proof

A39:
S
let m be Nat; :: thesis: ( S_{2}[m] implies S_{2}[m + 1] )

assume A36: S_{2}[m]
; :: thesis: S_{2}[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;assume A36: S

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

for i being Nat holds S

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

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

for i being Nat holds S

hence Sum H = (Sum F) + (Sum G) by A16, A19, A13, A12, A22; :: thesis: verum