let S, T be non empty RelStr ; :: thesis: for f being Function of S,T st f is isomorphic holds

for g being Function of T,S st g = f " holds

g is isomorphic

let f be Function of S,T; :: thesis: ( f is isomorphic implies for g being Function of T,S st g = f " holds

g is isomorphic )

assume A1: f is isomorphic ; :: thesis: for g being Function of T,S st g = f " holds

g is isomorphic

then A2: ex h being Function of T,S st

( h = f " & h is monotone ) by Def38;

let g be Function of T,S; :: thesis: ( g = f " implies g is isomorphic )

assume A3: g = f " ; :: thesis: g is isomorphic

for g being Function of T,S st g = f " holds

g is isomorphic

let f be Function of S,T; :: thesis: ( f is isomorphic implies for g being Function of T,S st g = f " holds

g is isomorphic )

assume A1: f is isomorphic ; :: thesis: for g being Function of T,S st g = f " holds

g is isomorphic

then A2: ex h being Function of T,S st

( h = f " & h is monotone ) by Def38;

let g be Function of T,S; :: thesis: ( g = f " implies g is isomorphic )

assume A3: g = f " ; :: thesis: g is isomorphic

per cases
( ( not T is empty & not S is empty ) or T is empty or S is empty )
;

:: according to WAYBEL_0:def 38end;

:: according to WAYBEL_0:def 38

case
( not T is empty & not S is empty )
; :: thesis: ( g is one-to-one & g is monotone & ex g being Function of S,T st

( g = g " & g is monotone ) )

( g = g " & g is monotone ) )

thus
( g is one-to-one & g is monotone )
by A1, A2, A3, FUNCT_1:40; :: thesis: ex g being Function of S,T st

( g = g " & g is monotone )

(f ") " = f by A1, FUNCT_1:43;

hence ex g being Function of S,T st

( g = g " & g is monotone ) by A1, A3; :: thesis: verum

end;( g = g " & g is monotone )

(f ") " = f by A1, FUNCT_1:43;

hence ex g being Function of S,T st

( g = g " & g is monotone ) by A1, A3; :: thesis: verum