theorem Th29: :: MESFUN16:29

for X, Y being non empty set
for Z being set
for f being PartFunc of [:X,Y:],Z
for x being Element of X
for y being Element of Y holds
( rng (ProjPMap1 (f,x)) c= rng f & rng (ProjPMap2 (f,y)) c= rng f )