let X be set ; :: thesis: (id X) * (id X) = id X
dom (id X) = X by RELAT_1:45;
hence (id X) * (id X) = id X by RELAT_1:51; :: thesis: verum