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
proof
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;
then Fseq is non-decreasing by VALUED_0:def 15;
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
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;
hence A13: seq is nonnegative by SUPINF_2:52; :: thesis: ( SUM seq = (SUM seq1) + (SUM seq2) & Sum seq = (Sum seq1) + (Sum seq2) )
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