let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for seq being ExtREAL_sequence st ( for m being Element of NAT holds
( ProjMap2 (f,m) is non-decreasing & seq . m = lim (ProjMap2 (f,m)) ) ) holds
( lim_in_cod2 (Partial_Sums_in_cod2 f) is non-decreasing & Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) )
let seq be ExtREAL_sequence; :: thesis: ( ( for m being Element of NAT holds
( ProjMap2 (f,m) is non-decreasing & seq . m = lim (ProjMap2 (f,m)) ) ) implies ( lim_in_cod2 (Partial_Sums_in_cod2 f) is non-decreasing & Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) ) )
assume A1: for m being Element of NAT holds
( ProjMap2 (f,m) is non-decreasing & seq . m = lim (ProjMap2 (f,m)) ) ; :: thesis: ( lim_in_cod2 (Partial_Sums_in_cod2 f) is non-decreasing & Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) )

now :: thesis: for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m))

let m be Element of NAT ; :: thesis: seq . m = lim_inf (ProjMap2 (f,m))
ProjMap2 (f,m) is non-decreasing by A1;
then ProjMap2 (f,m) is convergent by RINFSUP2:37;
then lim_inf (ProjMap2 (f,m)) = lim (ProjMap2 (f,m)) by RINFSUP2:41;
hence seq . m = lim_inf (ProjMap2 (f,m)) by A1; :: thesis: verum

end;

then A2: Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f)) by Th83;
A3: for n, m being Nat holds f . (n,m) <= seq . m

proof

let n, m be Nat; :: thesis: f . (n,m) <= seq . m
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
ProjMap2 (f,m1) is non-decreasing by A1;
then lim (ProjMap2 (f,m1)) = sup (ProjMap2 (f,m1)) by RINFSUP2:37;
then A4: seq . m = sup (ProjMap2 (f,m1)) by A1;
A5: n is Element of NAT by ORDINAL1:def 12;
dom (ProjMap2 (f,m1)) = NAT by FUNCT_2:def 1;
then (ProjMap2 (f,m1)) . n <= sup (rng (ProjMap2 (f,m1))) by A5, FUNCT_1:3, XXREAL_2:4;
then (ProjMap2 (f,m1)) . n <= sup (ProjMap2 (f,m1)) by RINFSUP2:def 1;
hence f . (n,m) <= seq . m by A4, A5, MESFUNC9:def 7; :: thesis: verum

end;

for n, m being Nat st m <= n holds
(lim_in_cod2 (Partial_Sums_in_cod2 f)) . m <= (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n

proof

let n, m be Nat; :: thesis: ( m <= n implies (lim_in_cod2 (Partial_Sums_in_cod2 f)) . m <= (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n )
assume C1: m <= n ; :: thesis: (lim_in_cod2 (Partial_Sums_in_cod2 f)) . m <= (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n
reconsider m1 = m, n1 = n as Element of NAT by ORDINAL1:def 12;
C2: ( (lim_in_cod2 (Partial_Sums_in_cod2 f)) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 f),m1)) & (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n = lim (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) ) by D1DEF6;
C3: ( ProjMap1 ((Partial_Sums_in_cod2 f),m1) is convergent & ProjMap1 ((Partial_Sums_in_cod2 f),n1) is convergent ) by RINFSUP2:37;
for k being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 f),m1)) . k <= (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . k

proof

let k be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod2 f),m1)) . k <= (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . k
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
( (ProjMap1 ((Partial_Sums_in_cod2 f),m1)) . k1 = (Partial_Sums_in_cod2 f) . (m1,k1) & (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . k1 = (Partial_Sums_in_cod2 f) . (n1,k1) ) by MESFUNC9:def 6;
hence (ProjMap1 ((Partial_Sums_in_cod2 f),m1)) . k <= (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . k by A1, C1, Th89; :: thesis: verum

end;

hence (lim_in_cod2 (Partial_Sums_in_cod2 f)) . m <= (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n by C2, C3, RINFSUP2:38; :: thesis: verum

end;

hence lim_in_cod2 (Partial_Sums_in_cod2 f) is non-decreasing by RINFSUP2:7; :: thesis: Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f))
then B1: lim_in_cod2 (Partial_Sums_in_cod2 f) is convergent by RINFSUP2:37;
then B3: Sum seq <= lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) by A2, RINFSUP2:41;
for n being Nat holds (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n <= Sum seq

proof

let n be Nat; :: thesis: (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n <= Sum seq
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
A6: (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n = lim (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) by D1DEF6;
A7: ProjMap1 ((Partial_Sums_in_cod2 f),n1) is convergent by RINFSUP2:37;
for m being Element of NAT holds 0 <= seq . m

proof

let m be Element of NAT ; :: thesis: 0 <= seq . m
for n being Nat holds 0. <= (ProjMap2 (f,m)) . n

proof

let n be Nat; :: thesis: 0. <= (ProjMap2 (f,m)) . n
n is Element of NAT by ORDINAL1:def 12;
hence 0. <= (ProjMap2 (f,m)) . n by SUPINF_2:39; :: thesis: verum

end;

then B2: 0. <= lim_inf (ProjMap2 (f,m)) by Th87;
ProjMap2 (f,m) is non-decreasing by A1;
then ProjMap2 (f,m) is convergent by RINFSUP2:37;
then lim_inf (ProjMap2 (f,m)) = lim (ProjMap2 (f,m)) by RINFSUP2:41;
hence 0 <= seq . m by B2, A1; :: thesis: verum

end;

then seq is nonnegative by SUPINF_2:39;
then Partial_Sums seq is non-decreasing by MESFUNC9:16;
then A8: Partial_Sums seq is convergent by RINFSUP2:37;
for m being Nat holds (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . m <= (Partial_Sums seq) . m

proof

let m be Nat; :: thesis: (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . m <= (Partial_Sums seq) . m
m is Element of NAT by ORDINAL1:def 12;
then (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . m = (Partial_Sums_in_cod2 f) . (n,m) by MESFUNC9:def 6;
hence (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) . m <= (Partial_Sums seq) . m by A3, Th85; :: thesis: verum

end;

then lim (ProjMap1 ((Partial_Sums_in_cod2 f),n1)) <= lim (Partial_Sums seq) by A7, A8, RINFSUP2:38;
hence (lim_in_cod2 (Partial_Sums_in_cod2 f)) . n <= Sum seq by A6, MESFUNC9:def 3; :: thesis: verum

end;

then lim_sup (lim_in_cod2 (Partial_Sums_in_cod2 f)) <= Sum seq by Th86;
then lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) <= Sum seq by B1, RINFSUP2:41;
hence Sum seq = lim (lim_in_cod2 (Partial_Sums_in_cod2 f)) by B3, XXREAL_0:1; :: thesis: verum