theorem Th30: :: MESFUN16:30

for X, Y being non empty set
for f being PartFunc of [:X,Y:],REAL
for x being Element of X
for y being Element of Y holds
( ProjPMap1 ((R_EAL f),x) is PartFunc of Y,REAL & ProjPMap1 (|.(R_EAL f).|,x) is PartFunc of Y,REAL & ProjPMap2 ((R_EAL f),y) is PartFunc of X,REAL & ProjPMap2 (|.(R_EAL f).|,y) is PartFunc of X,REAL )