let y1, y2 be set ; :: thesis: ( y1 in dom P & x in P . y1 & y2 in dom P & x in P . y2 implies y1 = y2 )
assume that
A5: y1 in dom P and
A6: x in P . y1 and
A7: y2 in dom P and
A8: x in P . y2 ; :: thesis: y1 = y2
A9: P . y1 in rng P by A5, FUNCT_1:def 3;
A10: P . y2 in rng P by A7, FUNCT_1:def 3;
P . y1 meets P . y2 by A6, A8, XBOOLE_0:3;
then P . y1 = P . y2 by A9, A10, EQREL_1:def 4;
hence y1 = y2 by A5, A7, FUNCT_1:def 4; :: thesis: verum