theorem Th27: :: MESFUN16:27

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