let X be set ; :: thesis: (id X) " = id X
dom (id X) = X by RELAT_1:71;
then A1: ((id X) " ) * (id X) = id X by Th61;
( dom ((id X) " ) = rng (id X) & rng (id X) = X ) by Th55, RELAT_1:71;
hence (id X) " = id X by A1, Th44; :: thesis: verum