let X1, X2 be non empty set ; :: thesis:
let x be Element of X1; :: thesis:
let y be Element of X2; :: thesis:
let f be PartFunc of [:X1,X2:],ExtREAL; :: thesis:
let a be ExtReal; :: thesis:

hereby :: thesis:

assume that
A2: [x,y] in dom f and
A3: f . (x,y) = a ; :: thesis:
y in X-section ((dom f),x) by A2, Th25;
hence y in dom (ProjPMap1 (f,x)) by Def3; :: thesis:
hence (ProjPMap1 (f,x)) . y = a by A3, Th26; :: thesis:

end;

hereby :: thesis:

assume that
A4: y in dom (ProjPMap1 (f,x)) and
A5: (ProjPMap1 (f,x)) . y = a ; :: thesis:
y in X-section ((dom f),x) by A4, Def3;
hence [x,y] in dom f by Th25; :: thesis:
thus f . (x,y) = a by A4, A5, Th26; :: thesis:

end;

hereby :: thesis:

assume that
A6: [x,y] in dom f and
A7: f . (x,y) = a ; :: thesis:
x in Y-section ((dom f),y) by A6, Th25;
hence x in dom (ProjPMap2 (f,y)) by Def4; :: thesis:
hence (ProjPMap2 (f,y)) . x = a by A7, Th26; :: thesis:

end;

assume that
A8: x in dom (ProjPMap2 (f,y)) and
A9: (ProjPMap2 (f,y)) . x = a ; :: thesis:
x in Y-section ((dom f),y) by A8, Def4;
hence [x,y] in dom f by Th25; :: thesis:
thus f . (x,y) = a by A8, A9, Th26; :: thesis: