let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: for k being Element of NAT holds
( ProjMap2 ((Partial_Sums_in_cod1 f),k) = Partial_Sums (ProjMap2 (f,k)) & ProjMap1 ((Partial_Sums_in_cod2 f),k) = Partial_Sums (ProjMap1 (f,k)) )
let k be Element of NAT ; :: thesis: ( ProjMap2 ((Partial_Sums_in_cod1 f),k) = Partial_Sums (ProjMap2 (f,k)) & ProjMap1 ((Partial_Sums_in_cod2 f),k) = Partial_Sums (ProjMap1 (f,k)) )

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

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

end;

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

now :: thesis: for n being Element of NAT holds (ProjMap1 ((Partial_Sums_in_cod2 f),k)) . n = (Partial_Sums (ProjMap1 (f,k))) . n

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

end;

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