let seq, seq1, seq2 be ExtREAL_sequence; :: thesis: ( seq1 is nonnegative & seq2 is nonnegative & ( for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ) implies ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) )

assume that

A1: seq1 is nonnegative and

A2: seq2 is nonnegative ; :: thesis: ( ex n being Nat st not seq . n = (seq1 . n) + (seq2 . n) or ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) )

reconsider Hseq = Ser seq2 as ExtREAL_sequence ;

reconsider Gseq = Ser seq1 as ExtREAL_sequence ;

reconsider Fseq = Ser seq as ExtREAL_sequence ;

assume A3: for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ; :: thesis: ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )

then A4: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ;

A5: for k being Nat holds Fseq . k = (Gseq . k) + (Hseq . k) by A1, A2, A4, MEASURE7:3;

for m, n being ExtReal st m in dom Fseq & n in dom Fseq & m <= n holds

Fseq . m <= Fseq . n

then A9: lim Fseq = sup Fseq by RINFSUP2:37;

Partial_Sums seq1 is non-decreasing by A1, MESFUNC9:16;

then Gseq is non-decreasing by Th1;

then A10: ( Gseq is convergent & lim Gseq = sup Gseq ) by RINFSUP2:37;

Partial_Sums seq2 is nonnegative by A2, MESFUNC9:16;

then A11: Hseq is nonnegative by Th1;

Partial_Sums seq2 is non-decreasing by A2, MESFUNC9:16;

then Hseq is non-decreasing by Th1;

then A14: ( Hseq is convergent & lim Hseq = sup Hseq ) by RINFSUP2:37;

Partial_Sums seq1 is nonnegative by A1, MESFUNC9:16;

then Gseq is nonnegative by Th1;

hence SUM seq = (SUM seq1) + (SUM seq2) by A10, A11, A14, A5, A9, MESFUNC9:11; :: thesis: Sum seq = (Sum seq1) + (Sum seq2)

then Sum seq = (SUM seq1) + (SUM seq2) by A13, Th2;

then Sum seq = (Sum seq1) + (SUM seq2) by A1, Th2;

hence Sum seq = (Sum seq1) + (Sum seq2) by A2, Th2; :: thesis: verum

assume that

A1: seq1 is nonnegative and

A2: seq2 is nonnegative ; :: thesis: ( ex n being Nat st not seq . n = (seq1 . n) + (seq2 . n) or ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) ) )

reconsider Hseq = Ser seq2 as ExtREAL_sequence ;

reconsider Gseq = Ser seq1 as ExtREAL_sequence ;

reconsider Fseq = Ser seq as ExtREAL_sequence ;

assume A3: for n being Nat holds seq . n = (seq1 . n) + (seq2 . n) ; :: thesis: ( seq is nonnegative & SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )

then A4: for n being Element of NAT holds seq . n = (seq1 . n) + (seq2 . n) ;

A5: for k being Nat holds Fseq . k = (Gseq . k) + (Hseq . k) by A1, A2, A4, MEASURE7:3;

for m, n being ExtReal st m in dom Fseq & n in dom Fseq & m <= n holds

Fseq . m <= Fseq . n

proof

then
Fseq is non-decreasing
by VALUED_0:def 15;
let m, n be ExtReal; :: thesis: ( m in dom Fseq & n in dom Fseq & m <= n implies Fseq . m <= Fseq . n )

assume that

A6: m in dom Fseq and

A7: n in dom Fseq and

A8: m <= n ; :: thesis: Fseq . m <= Fseq . n

( Gseq . m <= Gseq . n & Hseq . m <= Hseq . n ) by A1, A2, A6, A7, A8, MEASURE7:8;

then (Gseq . m) + (Hseq . m) <= (Gseq . n) + (Hseq . n) by XXREAL_3:36;

then Fseq . m <= (Gseq . n) + (Hseq . n) by A1, A2, A4, A6, MEASURE7:3;

hence Fseq . m <= Fseq . n by A1, A2, A4, A7, MEASURE7:3; :: thesis: verum

end;assume that

A6: m in dom Fseq and

A7: n in dom Fseq and

A8: m <= n ; :: thesis: Fseq . m <= Fseq . n

( Gseq . m <= Gseq . n & Hseq . m <= Hseq . n ) by A1, A2, A6, A7, A8, MEASURE7:8;

then (Gseq . m) + (Hseq . m) <= (Gseq . n) + (Hseq . n) by XXREAL_3:36;

then Fseq . m <= (Gseq . n) + (Hseq . n) by A1, A2, A4, A6, MEASURE7:3;

hence Fseq . m <= Fseq . n by A1, A2, A4, A7, MEASURE7:3; :: thesis: verum

then A9: lim Fseq = sup Fseq by RINFSUP2:37;

Partial_Sums seq1 is non-decreasing by A1, MESFUNC9:16;

then Gseq is non-decreasing by Th1;

then A10: ( Gseq is convergent & lim Gseq = sup Gseq ) by RINFSUP2:37;

Partial_Sums seq2 is nonnegative by A2, MESFUNC9:16;

then A11: Hseq is nonnegative by Th1;

now :: thesis: for n being object st n in dom seq holds

seq . n >= 0

hence A13:
seq is nonnegative
by SUPINF_2:52; :: thesis: ( SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )seq . n >= 0

let n be object ; :: thesis: ( n in dom seq implies seq . n >= 0 )

assume n in dom seq ; :: thesis: seq . n >= 0

then reconsider n9 = n as Element of NAT ;

A12: seq2 . n9 >= 0 by A2, SUPINF_2:51;

( seq . n = (seq1 . n9) + (seq2 . n9) & seq1 . n9 >= 0 ) by A1, A3, SUPINF_2:51;

hence seq . n >= 0 by A12; :: thesis: verum

end;assume n in dom seq ; :: thesis: seq . n >= 0

then reconsider n9 = n as Element of NAT ;

A12: seq2 . n9 >= 0 by A2, SUPINF_2:51;

( seq . n = (seq1 . n9) + (seq2 . n9) & seq1 . n9 >= 0 ) by A1, A3, SUPINF_2:51;

hence seq . n >= 0 by A12; :: thesis: verum

Partial_Sums seq2 is non-decreasing by A2, MESFUNC9:16;

then Hseq is non-decreasing by Th1;

then A14: ( Hseq is convergent & lim Hseq = sup Hseq ) by RINFSUP2:37;

Partial_Sums seq1 is nonnegative by A1, MESFUNC9:16;

then Gseq is nonnegative by Th1;

hence SUM seq = (SUM seq1) + (SUM seq2) by A10, A11, A14, A5, A9, MESFUNC9:11; :: thesis: Sum seq = (Sum seq1) + (Sum seq2)

then Sum seq = (SUM seq1) + (SUM seq2) by A13, Th2;

then Sum seq = (Sum seq1) + (SUM seq2) by A1, Th2;

hence Sum seq = (Sum seq1) + (Sum seq2) by A2, Th2; :: thesis: verum