let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for m being Element of NAT st ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) holds
( ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m) is convergent_to_+infty & lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) = +infty )
let m be Element of NAT ; :: thesis: ( ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) implies ( ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m) is convergent_to_+infty & lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) = +infty ) )
given k being Element of NAT such that A2: ( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) ; :: thesis: ( ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m) is convergent_to_+infty & lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) = +infty )
A5: for g being Real st 0 < g holds
ex N being Nat st
for n being Nat st N <= n holds
g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n

proof

let g be Real; :: thesis: ( 0 < g implies ex N being Nat st
for n being Nat st N <= n holds
g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n )
assume 0 < g ; :: thesis: ex N being Nat st
for n being Nat st N <= n holds
g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n
then consider N being Nat such that
A4: for n being Nat st N <= n holds
g <= (ProjMap1 ((Partial_Sums_in_cod2 f),k)) . n by A2, MESFUNC5:def 9;

now :: thesis: for n being Nat st N <= n holds
g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n

let n be Nat; :: thesis: ( N <= n implies g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n )
reconsider n1 = n as Element of NAT by ORDINAL1:def 12;
assume N <= n ; :: thesis: g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n
then g <= (ProjMap1 ((Partial_Sums_in_cod2 f),k)) . n by A4;
then A7: g <= (Partial_Sums_in_cod2 f) . (k,n1) by MESFUNC9:def 6;
(ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),n1)) . k <= (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),n1)) . m by A2, RINFSUP2:7;
then (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,n1) <= (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),n1)) . m by MESFUNC9:def 7;
then A10: (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,n1) <= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n1) by MESFUNC9:def 7;
(Partial_Sums_in_cod2 f) . (k,n1) <= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (k,n1) by Th76;
then A9: (Partial_Sums_in_cod2 f) . (k,n1) <= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n) by A10, XXREAL_0:2;
(ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n1 = (Partial_Sums f) . (m,n) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (m,n) by Lm8 ;
hence g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n by A7, A9, XXREAL_0:2; :: thesis: verum

end;

hence ex N being Nat st
for n being Nat st N <= n holds
g <= (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) . n ; :: thesis: verum

end;

hence ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m) is convergent_to_+infty by MESFUNC5:def 9; :: thesis: lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) = +infty
thus lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) = +infty by A5, MESFUNC5:def 9, MESFUNC9:7; :: thesis: verum