let x be object ; :: according to FUNCT_1:def 1 :: thesis: for y1, y2 being object st [x,y1] in id X & [x,y2] in id X holds
y1 = y2
let y1, y2 be object ; :: thesis: ( [x,y1] in id X & [x,y2] in id X implies y1 = y2 )
assume that
A1: [x,y1] in id X and
A2: [x,y2] in id X ; :: thesis: y1 = y2
x = y1 by A1, RELAT_1:def 10;
hence y1 = y2 by A2, RELAT_1:def 10; :: thesis: verum