let X1, X2 be non empty set ; :: thesis: for Y being set
for f being PartFunc of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
let Y be set ; :: thesis: for f being PartFunc of [:X1,X2:],Y
for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
let f be PartFunc of [:X1,X2:],Y; :: thesis: for x being Element of X1
for y being Element of X2 holds
( ( x in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . x = f . (x,y) ) & ( y in dom (ProjPMap1 (f,x)) implies (ProjPMap1 (f,x)) . y = f . (x,y) ) )
let c be Element of X1; :: thesis: for y being Element of X2 holds
( ( c in dom (ProjPMap2 (f,y)) implies (ProjPMap2 (f,y)) . c = f . (c,y) ) & ( y in dom (ProjPMap1 (f,c)) implies (ProjPMap1 (f,c)) . y = f . (c,y) ) )
let d be Element of X2; :: thesis: ( ( c in dom (ProjPMap2 (f,d)) implies (ProjPMap2 (f,d)) . c = f . (c,d) ) & ( d in dom (ProjPMap1 (f,c)) implies (ProjPMap1 (f,c)) . d = f . (c,d) ) )

hereby :: thesis: ( d in dom (ProjPMap1 (f,c)) implies (ProjPMap1 (f,c)) . d = f . (c,d) )

assume c in dom (ProjPMap2 (f,d)) ; :: thesis: (ProjPMap2 (f,d)) . c = f . (c,d)
then c in Y-section ((dom f),d) by Def4;
then c in { x where x is Element of X1 : [x,d] in dom f } by MEASUR11:def 5;
then ex x being Element of X1 st
( c = x & [x,d] in dom f ) ;
hence (ProjPMap2 (f,d)) . c = f . (c,d) by Def4; :: thesis: verum

end;

assume d in dom (ProjPMap1 (f,c)) ; :: thesis: (ProjPMap1 (f,c)) . d = f . (c,d)
then d in X-section ((dom f),c) by Def3;
then d in { y where y is Element of X2 : [c,y] in dom f } by MEASUR11:def 4;
then ex y being Element of X2 st
( d = y & [c,y] in dom f ) ;
hence (ProjPMap1 (f,c)) . d = f . (c,d) by Def3; :: thesis: verum