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 consider g being Function of T,S such that
A2: g = f " and
g is monotone by WAYBEL_0:def 38;
( rng f = the carrier of T & f is one-to-one ) by A1, WAYBEL_0:66;
hence f /" is isomorphic by A1, A2, TOPS_2:def 4, WAYBEL_0:68; :: thesis: verum