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 & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) holds
( ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m) is convergent_to_+infty & lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) = +infty )
let m be Element of NAT ; :: thesis: ( ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) implies ( ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m) is convergent_to_+infty & lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) = +infty ) )
given k being Element of NAT such that A1: ( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) ; :: thesis: ( ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m) is convergent_to_+infty & lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) = +infty )
A3: ProjMap2 ((Partial_Sums_in_cod1 f),k) = ProjMap2 ((Partial_Sums_in_cod1 (~ (~ f))),k) by DBLSEQ_2:7
.= ProjMap2 ((~ (Partial_Sums_in_cod2 (~ f))),k) by Th40
.= ProjMap1 ((Partial_Sums_in_cod2 (~ f)),k) by Th32 ;
ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 (~ f))),m) = ProjMap2 ((~ (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 (~ f)))),m) by Th32
.= ProjMap2 ((Partial_Sums_in_cod1 (~ (Partial_Sums_in_cod1 (~ f)))),m) by Th40
.= ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (~ (~ f)))),m) by Th40
.= ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m) by DBLSEQ_2:7 ;
hence ( ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m) is convergent_to_+infty & lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)),m)) = +infty ) by A3, A1, Th77; :: thesis: verum