for X1, X2, Y being non empty set
for F being Functional_Sequence of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 st F is with_the_same_dom holds
( ProjPMap1 (F,x) is with_the_same_dom & ProjPMap2 (F,y) is with_the_same_dom )