for X1, X2, Y being non empty set
for f being Function of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ProjPMap1 (f,x) = ProjMap1 (f,x) & ProjPMap2 (f,y) = ProjMap2 (f,y) )