let R be 1-sorted ; :: thesis: (id R) /" = id R
rng (id R) = [#] R by RELAT_1:45;
then id R is onto ;
hence (id R) /" = (id the carrier of R) " by TOPS_2:def 4
.= id R by FUNCT_1:45 ;
:: thesis: verum