theorem Th29: :: MESFUN12:29

for X1, X2 being non empty set
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)) )