let f be Function of [:NAT,NAT:],ExtREAL; :: thesis: ( ( not f is V183() or not f is V184() ) 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 V183() or not f is V184() ) ; :: 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