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