let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for m being Nat holds
( (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) )
let m be Nat; :: thesis: ( (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) )

hereby :: thesis: ( ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) implies (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty )

assume A2: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty ; :: thesis: ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty )

now :: thesis: ex k being Element of NAT st
( not k > m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty )

assume A3: for k being Element of NAT holds
( k > m or not ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) ; :: thesis: contradiction
defpred S₁[ Nat] means ( $1 <= m implies (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . $1 <> +infty );
(Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . 0 = (lim_in_cod2 (Partial_Sums_in_cod2 f)) . 0 by MESFUNC9:def 1
.= lim (ProjMap1 ((Partial_Sums_in_cod2 f),0)) by D1DEF6 ;
then A5: S₁[ 0 ] by A3, Th72;
A6: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A7: S₁[k] ; :: thesis: S₁[k + 1]
assume A8: k + 1 <= m ; :: thesis: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . (k + 1) <> +infty
A10: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . (k + 1) = ((Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . k) + ((lim_in_cod2 (Partial_Sums_in_cod2 f)) . (k + 1)) by MESFUNC9:def 1;

now :: thesis: not (lim_in_cod2 (Partial_Sums_in_cod2 f)) . (k + 1) = +infty

assume (lim_in_cod2 (Partial_Sums_in_cod2 f)) . (k + 1) = +infty ; :: thesis: contradiction
then lim (ProjMap1 ((Partial_Sums_in_cod2 f),(k + 1))) = +infty by D1DEF6;
hence contradiction by A3, A8, Th72; :: thesis: verum

end;

hence (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . (k + 1) <> +infty by A7, A8, NAT_1:13, A10, XXREAL_3:16; :: thesis: verum

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A5, A6);
hence contradiction by A2; :: thesis: verum

end;

hence ex k being Element of NAT st
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) ; :: thesis: verum

end;

given k being Element of NAT such that B1: ( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty ) ; :: thesis: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty
lim (ProjMap1 ((Partial_Sums_in_cod2 f),k)) = +infty by B1, MESFUNC9:7;
then B2: (lim_in_cod2 (Partial_Sums_in_cod2 f)) . k = +infty by D1DEF6;
B3: Partial_Sums_in_cod2 f is convergent_in_cod2 by RINFSUP2:37;
then lim_in_cod2 (Partial_Sums_in_cod2 f) is nonnegative by Th65;
then B5: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . k >= +infty by B2, Th4;
lim_in_cod2 (Partial_Sums_in_cod2 f) is nonnegative by B3, Th65;
then (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . k <= (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m by B1, RINFSUP2:7, MESFUNC9:16;
hence (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = +infty by B5, XXREAL_0:2, XXREAL_0:4; :: thesis: verum