let X be non empty set ; :: thesis: field (id X) = X
( dom (id X) = X & rng (id X) = X ) ;
then field (id X) = X \/ X by RELAT_1:def 6;
hence field (id X) = X ; :: thesis: verum