let X be set ; :: thesis: (id X) " = id X
dom (id X) = X ;
then A1: ((id X) ") * (id X) = id X by Th38;
( dom ((id X) ") = rng (id X) & rng (id X) = X ) by Th32;
hence (id X) " = id X by A1, Th23; :: thesis: verum