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

let y be Element of Y; :: thesis:
assume y in dom (ProjPMap1 ((R_EAL f),x)) ; :: thesis:
then A4: y in X-section ((dom f),x) by A1, MESFUN12:def 3;
X-section ((dom f),x) = { y where y is Element of Y : [x,y] in dom f } by MEASUR11:def 4;
then A5: ex y0 being Element of Y st
( y0 = y & [x,y0] in dom f ) by A4;
then (ProjPMap1 ((R_EAL f),x)) . y = (R_EAL f) . (x,y) by A1, MESFUN12:def 3;
then A6: (ProjPMap1 ((R_EAL f),x)) . y = f . (x,y) by MESFUNC5:def 7;
(R_EAL (ProjPMap1 (f,x))) . y = (ProjPMap1 (f,x)) . y by MESFUNC5:def 7;
hence (ProjPMap1 ((R_EAL f),x)) . y = (R_EAL (ProjPMap1 (f,x))) . y by A6, A5, MESFUN12:def 3; :: thesis:

end;

hence ProjPMap1 ((R_EAL f),x) = R_EAL (ProjPMap1 (f,x)) by A2, A3, PARTFUN1:5; :: thesis:
hence ProjPMap1 (|.(R_EAL f).|,x) = |.(R_EAL (ProjPMap1 (f,x))).| by MESFUN13:7; :: thesis:
for x being Element of X st x in dom (ProjPMap2 ((R_EAL f),y)) holds
(ProjPMap2 ((R_EAL f),y)) . x = (R_EAL (ProjPMap2 (f,y))) . x

let x be Element of X; :: thesis:
assume x in dom (ProjPMap2 ((R_EAL f),y)) ; :: thesis:
then A7: x in Y-section ((dom f),y) by A1, MESFUN12:def 4;
Y-section ((dom f),y) = { x where x is Element of X : [x,y] in dom f } by MEASUR11:def 5;
then A8: ex x0 being Element of X st
( x0 = x & [x0,y] in dom f ) by A7;
then (ProjPMap2 ((R_EAL f),y)) . x = (R_EAL f) . (x,y) by A1, MESFUN12:def 4;
then A9: (ProjPMap2 ((R_EAL f),y)) . x = f . (x,y) by MESFUNC5:def 7;
(R_EAL (ProjPMap2 (f,y))) . x = (ProjPMap2 (f,y)) . x by MESFUNC5:def 7;
hence (ProjPMap2 ((R_EAL f),y)) . x = (R_EAL (ProjPMap2 (f,y))) . x by A9, A8, MESFUN12:def 4; :: thesis:

end;

hence ProjPMap2 ((R_EAL f),y) = R_EAL (ProjPMap2 (f,y)) by A2, A3, PARTFUN1:5; :: thesis:
hence ProjPMap2 (|.(R_EAL f).|,y) = |.(R_EAL (ProjPMap2 (f,y))).| by MESFUN13:7; :: thesis: