let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( not f is without-infty or not f is without+infty ) implies ( ProjMap1 ((Partial_Sums f),0) = ProjMap1 ((Partial_Sums_in_cod2 f),0) & ProjMap2 ((Partial_Sums f),0) = ProjMap2 ((Partial_Sums_in_cod1 f),0) ) )
assume A0: ( not f is without-infty or not f is without+infty ) ; :: thesis: ( ProjMap1 ((Partial_Sums f),0) = ProjMap1 ((Partial_Sums_in_cod2 f),0) & ProjMap2 ((Partial_Sums f),0) = ProjMap2 ((Partial_Sums_in_cod1 f),0) )

A1: now :: thesis: for m being Element of NAT holds (ProjMap1 ((Partial_Sums f),0)) . m = (ProjMap1 ((Partial_Sums_in_cod2 f),0)) . m

let m be Element of NAT ; :: thesis: (ProjMap1 ((Partial_Sums f),0)) . m = (ProjMap1 ((Partial_Sums_in_cod2 f),0)) . m
(ProjMap1 ((Partial_Sums f),0)) . m = (Partial_Sums f) . (0,m) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 f)) . (0,m) by A0, Lm8, Lm9
.= (Partial_Sums_in_cod2 f) . (0,m) by DefRSM ;
hence (ProjMap1 ((Partial_Sums f),0)) . m = (ProjMap1 ((Partial_Sums_in_cod2 f),0)) . m by MESFUNC9:def 6; :: thesis: verum

end;

now :: thesis: for n being Element of NAT holds (ProjMap2 ((Partial_Sums f),0)) . n = (ProjMap2 ((Partial_Sums_in_cod1 f),0)) . n

let n be Element of NAT ; :: thesis: (ProjMap2 ((Partial_Sums f),0)) . n = (ProjMap2 ((Partial_Sums_in_cod1 f),0)) . n
(ProjMap2 ((Partial_Sums f),0)) . n = (Partial_Sums f) . (n,0) by MESFUNC9:def 7
.= (Partial_Sums_in_cod1 f) . (n,0) by DefCSM ;
hence (ProjMap2 ((Partial_Sums f),0)) . n = (ProjMap2 ((Partial_Sums_in_cod1 f),0)) . n by MESFUNC9:def 7; :: thesis: verum

end;

hence ( ProjMap1 ((Partial_Sums f),0) = ProjMap1 ((Partial_Sums_in_cod2 f),0) & ProjMap2 ((Partial_Sums f),0) = ProjMap2 ((Partial_Sums_in_cod1 f),0) ) by A1, FUNCT_2:63; :: thesis: verum