let x be object ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being object st [x,y1] in f ~ & [x,y2] in f ~ holds
y1 = y2
let y1, y2 be object ; :: 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 XTUPLE_0:def 12;
reconsider x = x as set by TARSKI:1;
A5: x = f . y2 by A3, Def2, A4;
A6: [y1,x] in f by A1, RELAT_1:def 7;
then A7: y1 in dom f by XTUPLE_0:def 12;
then x = f . y1 by A6, Def2;
hence y1 = y2 by A7, A4, A5, Def4; :: thesis: verum