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

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