let x be set ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being set st [x,y1] in f ~ & [x,y2] in f ~ holds
y1 = y2
let y1, y2 be set ; :: thesis: ( [x,y1] in f ~ & [x,y2] in f ~ implies y1 = y2 )
assume that
A1: [x,y1] in f ~ and
A2: [x,y2] in f ~ ; :: thesis: y1 = y2
A3: [y2,x] in f by A2, RELAT_1:def 7;
then A4: y2 in dom f by RELAT_1:def 4;
then A5: x = f . y2 by A3, Def4;
A6: [y1,x] in f by A1, RELAT_1:def 7;
then A7: y1 in dom f by RELAT_1:def 4;
then x = f . y1 by A6, Def4;
hence y1 = y2 by A7, A4, A5, Def8; :: thesis: verum