let X1, X2 be non empty set ; :: thesis:
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
let x be Element of X1; :: thesis:
let y be Element of X2; :: thesis:
assume A1: for z being Element of [:X1,X2:] st z in dom f holds
f . z = 0 ; :: thesis:

assume x in dom (ProjPMap2 (f,y)) ; :: thesis:
then x in Y-section ((dom f),y) by Def4;
then x in { x where x is Element of X1 : [x,y] in dom f } by MEASUR11:def 5;
then consider x1 being Element of X1 such that
A2: ( x1 = x & [x1,y] in dom f ) ;
f . (x1,y) = 0 by A1, A2;
hence (ProjPMap2 (f,y)) . x = 0 by A2, Def4; :: thesis:

end;

assume y in dom (ProjPMap1 (f,x)) ; :: thesis:
then y in X-section ((dom f),x) by Def3;
then y in { y where y is Element of X2 : [x,y] in dom f } by MEASUR11:def 4;
then consider y1 being Element of X2 such that
A3: ( y1 = y & [x,y1] in dom f ) ;
f . (x,y1) = 0 by A1, A3;
hence (ProjPMap1 (f,x)) . y = 0 by A3, Def3; :: thesis:

end;