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 that
A1: x1 in dom (id X) and
A2: x2 in dom (id X) ; :: thesis: ( not (id X) . x1 = (id X) . x2 or x1 = x2 )
x1 in X by A1, Th34;
then A3: (id X) . x1 = x1 by Th34;
x2 in X by A2, Th34;
hence ( not (id X) . x1 = (id X) . x2 or x1 = x2 ) by A3, Th34; :: thesis: verum