let S, T be non empty reflexive transitive RelStr ; :: thesis: for f being Function of S,T holds
( f is isomorphic iff ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) ) )
let f be Function of S,T; :: thesis: ( f is isomorphic iff ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) ) )

hereby :: thesis: ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) implies f is isomorphic )

assume A1: f is isomorphic ; :: thesis: ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) )
hence f is monotone ; :: thesis: ex g being monotone Function of T,S st
( f * g = id T & g * f = id S )
consider g being Function of T,S such that
A2: ( g = f " & g is monotone ) by A1, WAYBEL_0:def 38;
reconsider g = g as monotone Function of T,S by A2;
take g = g; :: thesis: ( f * g = id T & g * f = id S )
( f is one-to-one & rng f = the carrier of T ) by A1, WAYBEL_0:66;
hence ( f * g = id T & g * f = id S ) by A2, FUNCT_2:35; :: thesis: verum

end;

assume A3: f is monotone ; :: thesis: ( for g being monotone Function of T,S holds
( not f * g = id T or not g * f = id S ) or f is isomorphic )
given g being monotone Function of T,S such that A4: ( f * g = id T & g * f = id S ) ; :: thesis: f is isomorphic
A5: ( f is one-to-one & rng f = the carrier of T ) by A4, FUNCT_2:29;
then g = f " by A4, FUNCT_2:36;
hence f is isomorphic by A3, A5, WAYBEL_0:def 38; :: thesis: verum