let x1 be object ; :: according to FUNCT_1:def 4 :: thesis: for x2 being object st x1 in dom (id X) & x2 in dom (id X) & (id X) . x1 = (id X) . x2 holds
x1 = x2
let x2 be object ; :: 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;
then A3: (id X) . x1 = x1 by Th17;
x2 in X by A2;
hence ( not (id X) . x1 = (id X) . x2 or x1 = x2 ) by A3, Th17; :: thesis: verum