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:33;
rng (f ") = the carrier of S by A1, A3, FUNCT_1:33;
hence ( f " is Function of T,S & rng (f ") = the carrier of S ) by A4, FUNCT_2:1; :: thesis: verum