let r be Renaming of X,Z; :: thesis: ( r is X -defined & r is one-to-one )
dom r = X by defr;
hence r is X -defined by RELAT_1:def 18; :: thesis: r is one-to-one
thus r is one-to-one by defr; :: thesis: verum