let Rseq be Function of [:NAT,NAT:],REAL; :: thesis: ( ProjMap1 ((Partial_Sums Rseq),0) = ProjMap1 ((Partial_Sums_in_cod2 Rseq),0) & ProjMap2 ((Partial_Sums Rseq),0) = ProjMap2 ((Partial_Sums_in_cod1 Rseq),0) )

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

let m be Element of NAT ; :: thesis: (ProjMap1 ((Partial_Sums Rseq),0)) . m = (ProjMap1 ((Partial_Sums_in_cod2 Rseq),0)) . m
(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: verum

end;

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

let n be Element of NAT ; :: thesis: (ProjMap2 ((Partial_Sums Rseq),0)) . n = (ProjMap2 ((Partial_Sums_in_cod1 Rseq),0)) . n
(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: verum

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: verum