let f be V183() Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums f is convergent_in_cod1_to_-infty implies ex m being Element of NAT st ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty )
assume A1: Partial_Sums f is convergent_in_cod1_to_-infty ; :: thesis: ex m being Element of NAT st ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty
A3: ProjMap2 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),0) = ProjMap2 ((Partial_Sums f),0)
.= ProjMap2 ((Partial_Sums_in_cod1 f),0) by Th54 ;
assume for m being Element of NAT holds not ProjMap2 ((Partial_Sums_in_cod1 f),m) is convergent_to_-infty ; :: thesis: contradiction
hence contradiction by A1, A3; :: thesis: verum