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 " and
A3: g is monotone by A1, WAYBEL_0:def 38;
reconsider g = g as monotone Function of T,S by A3;
take g = g; :: thesis: ( f * g = id T & g * f = id S )
rng f = the carrier of T by A1, WAYBEL_0:66;
hence ( f * g = id T & g * f = id S ) by A1, A2, FUNCT_2:29; :: thesis: verum

end;

assume A4: 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 A5: f * g = id T and
A6: g * f = id S ; :: thesis: f is isomorphic
A7: f is one-to-one by A6, FUNCT_2:23;
f is onto by A5, FUNCT_2:23;
then rng f = the carrier of T by FUNCT_2:def 3;
then g = f " by A6, A7, FUNCT_2:30;
hence f is isomorphic by A4, A7, WAYBEL_0:def 38; :: thesis: verum