let X, Y be non empty set ; :: thesis: for f being PartFunc of [:X,Y:],REAL
for x being Element of X
for y being Element of Y holds
( ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| & ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| )
let f be PartFunc of [:X,Y:],REAL; :: thesis: for x being Element of X
for y being Element of Y holds
( ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| & ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| )
let x be Element of X; :: thesis: for y being Element of Y holds
( ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| & ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| )
let y be Element of Y; :: thesis: ( ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| & ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| )
A1: dom f = dom |.f.| by VALUED_1:def 11;
A2: ( dom (ProjPMap1 (f,x)) = dom |.(ProjPMap1 (f,x)).| & dom (ProjPMap2 (f,y)) = dom |.(ProjPMap2 (f,y)).| ) by VALUED_1:def 11;
A3: dom (ProjPMap1 (|.f.|,x)) = X-section ((dom f),x) by A1, MESFUN12:def 3;
then A4: dom (ProjPMap1 (|.f.|,x)) = dom |.(ProjPMap1 (f,x)).| by A2, MESFUN12:def 3;
for y being Element of Y st y in dom (ProjPMap1 (|.f.|,x)) holds
(ProjPMap1 (|.f.|,x)) . y = |.(ProjPMap1 (f,x)).| . y

proof

let y be Element of Y; :: thesis: ( y in dom (ProjPMap1 (|.f.|,x)) implies (ProjPMap1 (|.f.|,x)) . y = |.(ProjPMap1 (f,x)).| . y )
assume A5: y in dom (ProjPMap1 (|.f.|,x)) ; :: thesis: (ProjPMap1 (|.f.|,x)) . y = |.(ProjPMap1 (f,x)).| . y
then y in { y where y is Element of Y : [x,y] in dom f } by A3, MEASUR11:def 4;
then A6: ex y1 being Element of Y st
( y1 = y & [x,y1] in dom f ) ;
then A7: (ProjPMap1 (|.f.|,x)) . y = |.f.| . (x,y) by A1, MESFUN12:def 3;
(ProjPMap1 (f,x)) . y = f . (x,y) by A6, MESFUN12:def 3;
then |.(ProjPMap1 (f,x)).| . y = |.(f . [x,y]).| by A5, A4, VALUED_1:def 11;
hence (ProjPMap1 (|.f.|,x)) . y = |.(ProjPMap1 (f,x)).| . y by A1, A7, A6, VALUED_1:def 11; :: thesis: verum

end;

hence ProjPMap1 (|.f.|,x) = |.(ProjPMap1 (f,x)).| by A4, PARTFUN1:5; :: thesis: ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).|
A8: dom (ProjPMap2 (|.f.|,y)) = Y-section ((dom f),y) by A1, MESFUN12:def 4;
then A9: dom (ProjPMap2 (|.f.|,y)) = dom |.(ProjPMap2 (f,y)).| by A2, MESFUN12:def 4;
for x being Element of X st x in dom (ProjPMap2 (|.f.|,y)) holds
(ProjPMap2 (|.f.|,y)) . x = |.(ProjPMap2 (f,y)).| . x

proof

let x be Element of X; :: thesis: ( x in dom (ProjPMap2 (|.f.|,y)) implies (ProjPMap2 (|.f.|,y)) . x = |.(ProjPMap2 (f,y)).| . x )
assume A10: x in dom (ProjPMap2 (|.f.|,y)) ; :: thesis: (ProjPMap2 (|.f.|,y)) . x = |.(ProjPMap2 (f,y)).| . x
then x in { x where x is Element of X : [x,y] in dom f } by A8, MEASUR11:def 5;
then A11: ex x1 being Element of X st
( x1 = x & [x1,y] in dom f ) ;
then A12: (ProjPMap2 (|.f.|,y)) . x = |.f.| . (x,y) by A1, MESFUN12:def 4;
(ProjPMap2 (f,y)) . x = f . (x,y) by A11, MESFUN12:def 4;
then |.(ProjPMap2 (f,y)).| . x = |.(f . [x,y]).| by A10, A9, VALUED_1:def 11;
hence (ProjPMap2 (|.f.|,y)) . x = |.(ProjPMap2 (f,y)).| . x by A1, A12, A11, VALUED_1:def 11; :: thesis: verum

end;

hence ProjPMap2 (|.f.|,y) = |.(ProjPMap2 (f,y)).| by A9, PARTFUN1:5; :: thesis: verum