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