let X1, X2 be non empty set ; :: thesis: for x being Element of X1
for y being Element of X2
for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let x be Element of X1; :: thesis: for y being Element of X2
for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let y be Element of X2; :: thesis: for r being Real
for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let r be Real; :: thesis: for f being PartFunc of [:X1,X2:],ExtREAL holds
( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis: ( ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) & ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) )
( dom (ProjPMap1 ((r (#) f),x)) = X-section ((dom (r (#) f)),x) & dom (ProjPMap2 ((r (#) f),y)) = Y-section ((dom (r (#) f)),y) ) by Def3, Def4;
then A1: ( dom (ProjPMap1 ((r (#) f),x)) = X-section ((dom f),x) & dom (ProjPMap2 ((r (#) f),y)) = Y-section ((dom f),y) ) by MESFUNC1:def 6;
( dom (r (#) (ProjPMap1 (f,x))) = dom (ProjPMap1 (f,x)) & dom (r (#) (ProjPMap2 (f,y))) = dom (ProjPMap2 (f,y)) ) by MESFUNC1:def 6;
then A2: ( dom (r (#) (ProjPMap1 (f,x))) = X-section ((dom f),x) & dom (r (#) (ProjPMap2 (f,y))) = Y-section ((dom f),y) ) by Def3, Def4;

now :: thesis: for y being Element of X2 st y in dom (ProjPMap1 ((r (#) f),x)) holds
(ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . y

let y be Element of X2; :: thesis: ( y in dom (ProjPMap1 ((r (#) f),x)) implies (ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . y )
assume A3: y in dom (ProjPMap1 ((r (#) f),x)) ; :: thesis: (ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . y
then y in { y where y is Element of X2 : [x,y] in dom f } by A1, MEASUR11:def 4;
then A4: ex y1 being Element of X2 st
( y1 = y & [x,y1] in dom f ) ;
then A5: [x,y] in dom (r (#) f) by MESFUNC1:def 6;
A6: f . (x,y) = f . [x,y] ;
(r (#) (ProjPMap1 (f,x))) . y = r * ((ProjPMap1 (f,x)) . y) by A1, A2, A3, MESFUNC1:def 6
.= r * (f . [x,y]) by A4, A6, Def3
.= (r (#) f) . (x,y) by A5, MESFUNC1:def 6 ;
hence (ProjPMap1 ((r (#) f),x)) . y = (r (#) (ProjPMap1 (f,x))) . y by A5, Def3; :: thesis: verum

end;

hence ProjPMap1 ((r (#) f),x) = r (#) (ProjPMap1 (f,x)) by A1, A2, PARTFUN1:5; :: thesis: ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y))

now :: thesis: for x being Element of X1 st x in dom (ProjPMap2 ((r (#) f),y)) holds
(ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . x

let x be Element of X1; :: thesis: ( x in dom (ProjPMap2 ((r (#) f),y)) implies (ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . x )
assume A7: x in dom (ProjPMap2 ((r (#) f),y)) ; :: thesis: (ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . x
then x in { x where x is Element of X1 : [x,y] in dom f } by A1, MEASUR11:def 5;
then A8: ex x1 being Element of X1 st
( x1 = x & [x1,y] in dom f ) ;
then A9: [x,y] in dom (r (#) f) by MESFUNC1:def 6;
A10: f . (x,y) = f . [x,y] ;
(r (#) (ProjPMap2 (f,y))) . x = r * ((ProjPMap2 (f,y)) . x) by A1, A2, A7, MESFUNC1:def 6
.= r * (f . [x,y]) by A8, A10, Def4
.= (r (#) f) . (x,y) by A9, MESFUNC1:def 6 ;
hence (ProjPMap2 ((r (#) f),y)) . x = (r (#) (ProjPMap2 (f,y))) . x by A9, Def4; :: thesis: verum

end;

hence ProjPMap2 ((r (#) f),y) = r (#) (ProjPMap2 (f,y)) by A1, A2, PARTFUN1:5; :: thesis: verum