let f be without-infty Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums f is convergent_in_cod2_to_finite iff Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite )

hereby :: thesis: ( Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite implies Partial_Sums f is convergent_in_cod2_to_finite )

assume Partial_Sums f is convergent_in_cod2_to_finite ; :: thesis: Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite
then ~ (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)) is convergent_in_cod1_to_finite by Th36;
then Partial_Sums_in_cod1 (~ (Partial_Sums_in_cod1 f)) is convergent_in_cod1_to_finite by Th40;
then Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (~ f)) is convergent_in_cod1_to_finite by Th40;
then Partial_Sums (~ f) is convergent_in_cod1_to_finite by Lm8;
then Partial_Sums_in_cod1 (~ f) is convergent_in_cod1_to_finite by Th79;
then ~ (Partial_Sums_in_cod2 f) is convergent_in_cod1_to_finite by Th40;
hence Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite by Th36; :: thesis: verum

end;

assume Partial_Sums_in_cod2 f is convergent_in_cod2_to_finite ; :: thesis: Partial_Sums f is convergent_in_cod2_to_finite
then ~ (Partial_Sums_in_cod2 f) is convergent_in_cod1_to_finite by Th36;
then Partial_Sums_in_cod1 (~ f) is convergent_in_cod1_to_finite by Th40;
then Partial_Sums (~ f) is convergent_in_cod1_to_finite by Th79;
then Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (~ f)) is convergent_in_cod1_to_finite by Lm8;
then Partial_Sums_in_cod1 (~ (Partial_Sums_in_cod1 f)) is convergent_in_cod1_to_finite by Th40;
then ~ (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)) is convergent_in_cod1_to_finite by Th40;
hence Partial_Sums f is convergent_in_cod2_to_finite by Th36; :: thesis: verum