let Rseq be Function of [:NAT,NAT:],REAL; :: thesis:

A1: now :: thesis:

let m be Element of NAT ; :: thesis:
(ProjMap1 ((Partial_Sums Rseq),0)) . m = (Partial_Sums Rseq) . (0,m) by MESFUNC9:def 6
.= (Partial_Sums_in_cod1 (Partial_Sums_in_cod2 Rseq)) . (0,m) by th103a
.= (Partial_Sums_in_cod2 Rseq) . (0,m) by DefRS ;
hence (ProjMap1 ((Partial_Sums Rseq),0)) . m = (ProjMap1 ((Partial_Sums_in_cod2 Rseq),0)) . m by MESFUNC9:def 6; :: thesis:

end;

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

end;

hence ( ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) & ProjMap2 ((Partial_Sums Rseq),0) = ProjMap2 ((Partial_Sums_in_cod1 Rseq),0) ) by A1; :: thesis: