let f be nonnegative Function of [:NAT,NAT:],ExtREAL; 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; ( (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 ) )
given k being Element of NAT such that B1:
( k <= m & ProjMap1 ((Partial_Sums_in_cod2 f),k) is convergent_to_+infty )
; (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; verum