:: deftheorem defr defines Renaming FIELD_5:def 5 :
for X being non empty set
for Z being set
for b₃ being Function holds
( b₃ is Renaming of X,Z iff ( dom b₃ = X & b₃ is one-to-one & (rng b₃) /\ (X \/ Z) = {} ) );