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 A1: f is isomorphic ; :: thesis: ( f " is Function of T,S & rng (f " ) = the carrier of S )
then A2: rng f = the carrier of T by Th66;
A3: dom f = the carrier of S by FUNCT_2:def 1;
A4: dom (f " ) = the carrier of T by A1, A2, FUNCT_1:55;
rng (f " ) = the carrier of S by A1, A3, FUNCT_1:55;
hence ( f " is Function of T,S & rng (f " ) = the carrier of S ) by A4, FUNCT_2:3; :: thesis: verum