let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for m being Nat holds
( ( for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty )
let m be Nat; :: thesis: ( ( for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) iff for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty )

hereby :: thesis: ( ( for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty ) implies for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty )

assume A1: for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ; :: thesis: for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty

hereby :: thesis: verum

let k be Element of NAT ; :: thesis: ( k <= m implies lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty )
assume k <= m ; :: thesis: lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty
then not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty by A1;
then ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_finite_number by Th62;
then ex g being Real st
( lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) = g & ( for p being Real st 0 < p holds
ex n being Nat st
for m being Nat st n <= m holds
|.(((ProjMap2 ((Partial_Sums_in_cod1 f),k)) . m) - (lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)))).| < p ) ) by MESFUNC9:7;
hence lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty by XREAL_0:def 1, XXREAL_0:9; :: thesis: verum

end;

end;

assume A2: for k being Element of NAT st k <= m holds
lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty ; :: thesis: for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty

now :: thesis: for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty

let k be Element of NAT ; :: thesis: ( k <= m implies not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty )
assume k <= m ; :: thesis: not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty
then lim (ProjMap2 ((Partial_Sums_in_cod1 f),k)) < +infty by A2;
hence not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty by MESFUNC9:7; :: thesis: verum

end;

hence for k being Element of NAT st k <= m holds
not ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ; :: thesis: verum