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