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