let f be Function of [:NAT,NAT:],ExtREAL; :: thesis:
let k be Element of NAT ; :: thesis:

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

end;

hence ProjMap2 ((Partial_Sums_in_cod1 f),k) = Partial_Sums (ProjMap2 (f,k)) by FUNCT_2:def 8; :: thesis:

let n be Element of NAT ; :: thesis:
(ProjMap1 ((Partial_Sums_in_cod2 f),k)) . n = (Partial_Sums_in_cod2 f) . (k,n) by MESFUNC9:def 6;
hence (ProjMap1 ((Partial_Sums_in_cod2 f),k)) . n = (Partial_Sums (ProjMap1 (f,k))) . n by Th43; :: thesis:

end;

hence ProjMap1 ((Partial_Sums_in_cod2 f),k) = Partial_Sums (ProjMap1 (f,k)) by FUNCT_2:def 8; :: thesis: