let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis:
let seq be ExtREAL_sequence; :: thesis:
assume A1: for m being Element of NAT holds seq . m = lim_inf (ProjMap2 (f,m)) ; :: thesis:
A2: for m, N, n being Element of NAT st n >= N holds
(inferior_realsequence (ProjMap2 (f,m))) . N <= f . (n,m)

proof

let m be Element of NAT ; :: thesis:
let N, n be Element of NAT ; :: thesis:
assume n >= N ; :: thesis:
then A4: (inferior_realsequence (ProjMap2 (f,m))) . N <= (inferior_realsequence (ProjMap2 (f,m))) . n by RINFSUP2:7;
(inferior_realsequence (ProjMap2 (f,m))) . n <= (ProjMap2 (f,m)) . n by RINFSUP2:8;
then (inferior_realsequence (ProjMap2 (f,m))) . n <= f . (n,m) by MESFUNC9:def 7;
hence (inferior_realsequence (ProjMap2 (f,m))) . N <= f . (n,m) by A4, XXREAL_0:2; :: thesis:

end;

deffunc H₁( Element of NAT ) -> Element of bool [:omega,ExtREAL:] = inferior_realsequence (ProjMap2 (f,$1));
deffunc H₂( Element of NAT , Element of NAT ) -> Element of ExtREAL = (inferior_realsequence (ProjMap2 (f,$2))) . $1;
consider g being Function of [:NAT,NAT:],ExtREAL such that
A5: for n, m being Element of NAT holds g . (n,m) = H₂(n,m) from BINOP_1:sch 4();

now :: thesis:

let z be object ; :: thesis:

per cases ;

suppose z in dom g ; :: thesis:

then consider n, m being object such that
D1: ( n in NAT & m in NAT & z = [n,m] ) by ZFMISC_1:def 2;
reconsider n = n, m = m as Element of NAT by D1;
g . (n,m) = (inferior_realsequence (ProjMap2 (f,m))) . n by A5;
then consider Y being non empty Subset of ExtREAL such that
D2: ( Y = { ((ProjMap2 (f,m)) . k) where k is Nat : n <= k } & g . z = inf Y ) by D1, RINFSUP2:def 6;
for x being ExtReal st x in Y holds
0 <= x

proof

let x be ExtReal; :: thesis:
assume x in Y ; :: thesis:
then ex k being Nat st
( x = (ProjMap2 (f,m)) . k & n <= k ) by D2;
hence 0 <= x by SUPINF_2:51; :: thesis:

end;

then 0 is LowerBound of Y by XXREAL_2:def 2;
hence 0 <= g . z by D2, XXREAL_2:def 4; :: thesis:

end;

suppose not z in dom g ; :: thesis:

hence 0 <= g . z by FUNCT_1:def 2; :: thesis:

end;

then g is nonnegative by SUPINF_2:51;
then reconsider g = g as nonnegative without-infty Function of [:NAT,NAT:],ExtREAL ;
A6: for m, N, n being Element of NAT st n >= N holds
(Partial_Sums_in_cod2 g) . (N,m) <= (Partial_Sums_in_cod2 f) . (n,m)

proof

let m be Element of NAT ; :: thesis:
let N, n be Element of NAT ; :: thesis:
assume A7: n >= N ; :: thesis:
defpred S₁[ Nat] means (Partial_Sums_in_cod2 g) . (N,$1) <= (Partial_Sums_in_cod2 f) . (n,$1);
A8: (Partial_Sums_in_cod2 g) . (N,0) = g . (N,0) by DefCSM
.= (inferior_realsequence (ProjMap2 (f,0))) . N by A5 ;
(Partial_Sums_in_cod2 f) . (n,0) = f . (n,0) by DefCSM;
then A9: S₁[ 0 ] by A2, A7, A8;
A10: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume A11: S₁[k] ; :: thesis:
g . (N,(k1 + 1)) = (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . N by A5;
then A12: g . (N,(k1 + 1)) <= f . (n,(k1 + 1)) by A2, A7;
( (Partial_Sums_in_cod2 g) . (N,(k + 1)) = ((Partial_Sums_in_cod2 g) . (N,k)) + (g . (N,(k1 + 1))) & (Partial_Sums_in_cod2 f) . (n,(k + 1)) = ((Partial_Sums_in_cod2 f) . (n,k)) + (f . (n,(k1 + 1))) ) by DefCSM;
hence S₁[k + 1] by A11, A12, XXREAL_3:36; :: thesis:

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A9, A10);
hence (Partial_Sums_in_cod2 g) . (N,m) <= (Partial_Sums_in_cod2 f) . (n,m) ; :: thesis:

end;

A13: for m, N, n being Element of NAT st n >= N holds
(Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n

proof

let m be Element of NAT ; :: thesis:
let N, n be Element of NAT ; :: thesis:
assume A14: n >= N ; :: thesis:
consider Y being non empty Subset of ExtREAL such that
A15: ( Y = { ((ProjMap2 ((Partial_Sums_in_cod2 f),m)) . k) where k is Nat : n <= k } & (inferior_realsequence (ProjMap2 ((Partial_Sums_in_cod2 f),m))) . n = inf Y ) by RINFSUP2:def 6;
for x being ExtReal st x in Y holds
(Partial_Sums_in_cod2 g) . (N,m) <= x

proof

let x be ExtReal; :: thesis:
assume x in Y ; :: thesis:
then consider k being Nat such that
A17: ( x = (ProjMap2 ((Partial_Sums_in_cod2 f),m)) . k & n <= k ) by A15;
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
A18: N <= k1 by A14, A17, XXREAL_0:2;
x = (Partial_Sums_in_cod2 f) . (k1,m) by A17, MESFUNC9:def 7;
hence (Partial_Sums_in_cod2 g) . (N,m) <= x by A6, A18; :: thesis:

end;

then (Partial_Sums_in_cod2 g) . (N,m) is LowerBound of Y by XXREAL_2:def 2;
then A19: (Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (ProjMap2 ((Partial_Sums_in_cod2 f),m))) . n by A15, XXREAL_2:def 4;
consider Z being non empty Subset of ExtREAL such that
A20: ( Z = { ((lim_in_cod2 (Partial_Sums_in_cod2 f)) . k) where k is Nat : n <= k } & (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n = inf Z ) by RINFSUP2:def 6;
for z being ExtReal st z in Z holds
ex y being ExtReal st
( y in Y & y <= z )

proof

end;

then inf Y <= inf Z by XXREAL_2:64;
hence (Partial_Sums_in_cod2 g) . (N,m) <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n by A15, A20, A19, XXREAL_0:2; :: thesis:

end;

defpred S₁[ Nat] means for m being Element of NAT st m = $1 holds
(Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m));

now :: thesis:

let m be Element of NAT ; :: thesis:
assume A24: m = 0 ; :: thesis:
then (Partial_Sums seq) . m = seq . 0 by MESFUNC9:def 1
.= lim_inf (ProjMap2 (f,0)) by A1
.= sup (inferior_realsequence (ProjMap2 (f,0))) by RINFSUP2:def 9 ;
then A26: (Partial_Sums seq) . m = lim (inferior_realsequence (ProjMap2 (f,0))) by RINFSUP2:37;

now :: thesis:

let n be Element of NAT ; :: thesis:
(ProjMap2 ((Partial_Sums_in_cod2 g),0)) . n = (Partial_Sums_in_cod2 g) . (n,0) by MESFUNC9:def 7
.= g . (n,0) by DefCSM
.= (inferior_realsequence (ProjMap2 (f,0))) . n by A5 ;
hence (inferior_realsequence (ProjMap2 (f,0))) . n = (ProjMap2 ((Partial_Sums_in_cod2 g),0)) . n ; :: thesis:

end;

hence (Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m)) by A24, A26, FUNCT_2:63; :: thesis:

end;

then A28: S₁[ 0 ] ;
P1: for m being Element of NAT holds ProjMap2 ((Partial_Sums_in_cod2 g),m) is convergent

proof

let m be Element of NAT ; :: thesis:
for j, i being Nat st i <= j holds
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i <= (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j

proof

proof

let l be Nat; :: thesis:
reconsider l1 = l as Element of NAT by ORDINAL1:def 12;
assume B7: S₂[l] ; :: thesis:
( g . (i,(l + 1)) = (inferior_realsequence (ProjMap2 (f,(l1 + 1)))) . i1 & g . (j,(l + 1)) = (inferior_realsequence (ProjMap2 (f,(l1 + 1)))) . j1 ) by A5;
then B8: g . (i,(l + 1)) <= g . (j,(l + 1)) by B2, RINFSUP2:7;
( (Partial_Sums_in_cod2 g) . (i,(l + 1)) = ((Partial_Sums_in_cod2 g) . (i,l)) + (g . (i,(l + 1))) & (Partial_Sums_in_cod2 g) . (j,(l + 1)) = ((Partial_Sums_in_cod2 g) . (j,l)) + (g . (j,(l + 1))) ) by DefCSM;
hence S₂[l + 1] by B7, B8, XXREAL_3:36; :: thesis:

end;

for l being Nat holds S₂[l] from NAT_1:sch 2(B5, B6);
hence (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i <= (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . j by B3; :: thesis:

end;

then ProjMap2 ((Partial_Sums_in_cod2 g),m) is non-decreasing by RINFSUP2:7;
hence ProjMap2 ((Partial_Sums_in_cod2 g),m) is convergent by RINFSUP2:37; :: thesis:

end;

A29: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
reconsider k1 = k as Element of NAT by ORDINAL1:def 12;
assume A30: S₁[k] ; :: thesis:

now :: thesis:

let m be Element of NAT ; :: thesis:
assume B00: m = k + 1 ; :: thesis:
then B0: (Partial_Sums seq) . m = ((Partial_Sums seq) . k) + (seq . (k + 1)) by MESFUNC9:def 1
.= (lim (ProjMap2 ((Partial_Sums_in_cod2 g),k1))) + (seq . (k + 1)) by A30
.= (lim (ProjMap2 ((Partial_Sums_in_cod2 g),k1))) + (lim_inf (ProjMap2 (f,(k + 1)))) by A1 ;
B1: lim_inf (ProjMap2 (f,(k + 1))) = sup (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) by RINFSUP2:def 9
.= lim (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) by RINFSUP2:37 ;
B9: ProjMap2 ((Partial_Sums_in_cod2 g),k1) is convergent by P1;
B10: inferior_realsequence (ProjMap2 (f,(k1 + 1))) is convergent by RINFSUP2:37;
for n being object st n in dom (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) holds
0. <= (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . n

proof

let n be object ; :: thesis:
assume n in dom (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) ; :: thesis:
then g . (n,(k1 + 1)) = (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . n by A5;
hence 0. <= (inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . n by SUPINF_2:51; :: thesis:

end;

then C2: inferior_realsequence (ProjMap2 (f,(k1 + 1))) is nonnegative by SUPINF_2:52;
for i being Nat holds (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i = ((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i) + ((inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . i)

proof

let i be Nat; :: thesis:
reconsider i1 = i as Element of NAT by ORDINAL1:def 12;
(ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i1 = (Partial_Sums_in_cod2 g) . (i,m) by MESFUNC9:def 7
.= ((Partial_Sums_in_cod2 g) . (i,k)) + (g . (i,(k + 1))) by B00, DefCSM
.= ((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i1) + (g . (i,(k + 1))) by MESFUNC9:def 7 ;
hence (ProjMap2 ((Partial_Sums_in_cod2 g),m)) . i = ((ProjMap2 ((Partial_Sums_in_cod2 g),k1)) . i) + ((inferior_realsequence (ProjMap2 (f,(k1 + 1)))) . i) by A5; :: thesis:

end;

hence (Partial_Sums seq) . m = lim (ProjMap2 ((Partial_Sums_in_cod2 g),m)) by B0, B1, B9, B10, C2, MESFUNC9:11; :: thesis:

end;

hence S₁[k + 1] ; :: thesis:

end;

A30: for k being Nat holds S₁[k] from NAT_1:sch 2(A28, A29);
A31: for m being Nat holds (Partial_Sums seq) . m <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f))

proof

let m be Nat; :: thesis:
reconsider m1 = m as Element of NAT by ORDINAL1:def 12;
A32: for n being Nat holds (ProjMap2 ((Partial_Sums_in_cod2 g),m1)) . n <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n

proof

let n be Nat; :: thesis:
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
(ProjMap2 ((Partial_Sums_in_cod2 g),m1)) . n1 = (Partial_Sums_in_cod2 g) . (n,m) by MESFUNC9:def 7;
hence (ProjMap2 ((Partial_Sums_in_cod2 g),m1)) . n <= (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) . n by A13; :: thesis:

end;

A33: ProjMap2 ((Partial_Sums_in_cod2 g),m1) is convergent by P1;
inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f)) is convergent by RINFSUP2:37;
then lim (ProjMap2 ((Partial_Sums_in_cod2 g),m1)) <= lim (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) by A32, A33, RINFSUP2:38;
then (Partial_Sums seq) . m <= lim (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) by A30;
then (Partial_Sums seq) . m <= sup (inferior_realsequence (lim_in_cod2 (Partial_Sums_in_cod2 f))) by RINFSUP2:37;
hence (Partial_Sums seq) . m <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f)) by RINFSUP2:def 9; :: thesis:

end;

for m being object st m in dom seq holds
0 <= seq . m

proof

let m be object ; :: thesis:
assume m in dom seq ; :: thesis:
then reconsider m1 = m as Element of NAT ;
E1: seq . m = lim_inf (ProjMap2 (f,m1)) by A1
.= sup (inferior_realsequence (ProjMap2 (f,m1))) by RINFSUP2:def 9 ;
for n being object st n in dom (inferior_realsequence (ProjMap2 (f,m1))) holds
0. <= (inferior_realsequence (ProjMap2 (f,m1))) . n

proof

let n be object ; :: thesis:
assume n in dom (inferior_realsequence (ProjMap2 (f,m1))) ; :: thesis:
then g . (n,m1) = (inferior_realsequence (ProjMap2 (f,m1))) . n by A5;
hence 0. <= (inferior_realsequence (ProjMap2 (f,m1))) . n by SUPINF_2:51; :: thesis:

end;

then (inferior_realsequence (ProjMap2 (f,m1))) . 0 >= 0 by SUPINF_2:51, SUPINF_2:52;
hence 0 <= seq . m by E1, RINFSUP2:23; :: thesis:

end;

then seq is nonnegative by SUPINF_2:52;
then Partial_Sums seq is non-decreasing by MESFUNC9:16;
then lim (Partial_Sums seq) <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f)) by A31, MESFUNC9:9, RINFSUP2:37;
hence Sum seq <= lim_inf (lim_in_cod2 (Partial_Sums_in_cod2 f)) by MESFUNC9:def 3; :: thesis: