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