let S, T be non empty RelStr ; :: thesis: for f being Function of S,T st f is isomorphic holds
f /" is isomorphic
let f be Function of S,T; :: thesis: ( f is isomorphic implies f /" is isomorphic )
assume A1: f is isomorphic ; :: thesis: f /" is isomorphic
then ( ex g being Function of T,S st
( g = f " & g is monotone ) & rng f = the carrier of T ) by WAYBEL_0:66, WAYBEL_0:def 38;
hence f /" is isomorphic by A1, TOPS_2:def 4, WAYBEL_0:68; :: thesis: verum