let f be nonnegative Function of [:NAT,NAT:],ExtREAL; :: thesis: ( Partial_Sums f is convergent_in_cod2_to_finite implies for m being Element of NAT holds (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) )
assume Partial_Sums f is convergent_in_cod2_to_finite ; :: thesis: for m being Element of NAT holds (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m))
then Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f) is convergent_in_cod2_to_finite by Lm8;
then ~ (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) is convergent_in_cod1_to_finite by Th36;
then Partial_Sums_in_cod2 (~ (Partial_Sums_in_cod2 f)) is convergent_in_cod1_to_finite by Th40;
then A1: Partial_Sums (~ f) is convergent_in_cod1_to_finite by Th40;
hereby :: thesis: verum
let m be Element of NAT ; :: thesis: (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m))
lim_in_cod2 (Partial_Sums_in_cod2 f) = lim_in_cod1 (~ (Partial_Sums_in_cod2 f)) by Th38
.= lim_in_cod1 (Partial_Sums_in_cod1 (~ f)) by Th40 ;
then (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap2 ((Partial_Sums_in_cod1 (Partial_Sums_in_cod2 (~ f))),m)) by A1, Th80
.= lim (ProjMap2 ((Partial_Sums_in_cod1 (~ (Partial_Sums_in_cod1 f))),m)) by Th40
.= lim (ProjMap2 ((~ (Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f))),m)) by Th40 ;
hence (Partial_Sums (lim_in_cod2 (Partial_Sums_in_cod2 f))) . m = lim (ProjMap1 ((Partial_Sums_in_cod2 (Partial_Sums_in_cod1 f)),m)) by Th32; :: thesis: verum
end;