( dom (id R) = [#] R & rng (id R) = [#] R ) by RELAT_1:71;
hence (id R) /" is one-to-one by TOPS_2:63; :: thesis: verum