theorem Th28: :: MESFUN16:28

for X, Y being non empty set
for A being Subset of X
for B being Subset of Y
for y being Element of Y
for f being PartFunc of [:X,Y:],REAL st dom f = [:A,B:] holds
( ( y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = A & dom (ProjPMap2 (|.(R_EAL f).|,y)) = A ) ) & ( not y in B implies ( dom (ProjPMap2 ((R_EAL f),y)) = {} & dom (ProjPMap2 (|.(R_EAL f).|,y)) = {} ) ) )