let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: for m being Nat holds
( (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) )
let m be Nat; :: thesis: ( (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty iff ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) )
hereby :: thesis: ( ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) implies (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty )
assume A1: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty ; :: thesis: ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty )
lim_in_cod1 (Partial_Sums_in_cod1 f) = lim_in_cod2 (~ (Partial_Sums_in_cod1 f)) by Th38
.= lim_in_cod2 (Partial_Sums_in_cod2 (~ f)) by Th40 ;
then consider k being Element of NAT such that
A2: ( k <= m & ProjMap1 ((Partial_Sums_in_cod2 (~ f)),k) is convergent_to_+infty ) by A1, Th74;
ProjMap1 ((Partial_Sums_in_cod2 (~ f)),k) = ProjMap2 ((~ (Partial_Sums_in_cod2 (~ f))),k) by Th32
.= ProjMap2 ((Partial_Sums_in_cod1 (~ (~ f))),k) by Th40
.= ProjMap2 ((Partial_Sums_in_cod1 f),k) by DBLSEQ_2:7 ;
hence ex k being Element of NAT st
( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) by A2; :: thesis: verum
end;
given k being Element of NAT such that A3: ( k <= m & ProjMap2 ((Partial_Sums_in_cod1 f),k) is convergent_to_+infty ) ; :: thesis: (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty
A4: 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 ;
lim_in_cod1 (Partial_Sums_in_cod1 f) = lim_in_cod2 (~ (Partial_Sums_in_cod1 f)) by Th38
.= lim_in_cod2 (Partial_Sums_in_cod2 (~ f)) by Th40 ;
hence (Partial_Sums (lim_in_cod1 (Partial_Sums_in_cod1 f))) . m = +infty by A3, A4, Th74; :: thesis: verum