for S, T being non empty RelStr
for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S & rng (f ") = the carrier of S )