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

( 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