let X be set ; :: thesis: id X is one-to-one
let x1 be set ; :: according to FUNCT_1:def 8 :: thesis: for x2 being set st x1 in dom (id X) & x2 in dom (id X) & (id X) . x1 = (id X) . x2 holds
x1 = x2
let x2 be set ; :: thesis: ( x1 in dom (id X) & x2 in dom (id X) & (id X) . x1 = (id X) . x2 implies x1 = x2 )
assume ( x1 in dom (id X) & x2 in dom (id X) ) ; :: thesis: ( not (id X) . x1 = (id X) . x2 or x1 = x2 )
then ( x1 in X & x2 in X ) by Th34;
then ( (id X) . x1 = x1 & (id X) . x2 = x2 ) by Th34;
hence ( not (id X) . x1 = (id X) . x2 or x1 = x2 ) ; :: thesis: verum