let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis:
let m be Nat; :: thesis:

hereby :: thesis:

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:

hereby :: thesis:

let k be Element of NAT ; :: thesis:
assume k <= m ; :: thesis:
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:

end;

end;

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

let k be Element of NAT ; :: thesis:
assume k <= m ; :: thesis:
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:

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: