let S, T be non empty RelStr ; :: thesis: for f being Function of S,T st f is isomorphic holds
( f " is Function of T,S & rng (f " ) = the carrier of S )
let f be Function of S,T; :: thesis: ( f is isomorphic implies ( f " is Function of T,S & rng (f " ) = the carrier of S ) )
assume f is isomorphic ; :: thesis: ( f " is Function of T,S & rng (f " ) = the carrier of S )
then ( f is one-to-one & rng f = the carrier of T & dom f = the carrier of S ) by Th66, FUNCT_2:def 1;
then ( dom (f " ) = the carrier of T & rng (f " ) = the carrier of S ) by FUNCT_1:55;
hence ( f " is Function of T,S & rng (f " ) = the carrier of S ) by FUNCT_2:3; :: thesis: verum