let S, T be non empty reflexive transitive RelStr ; 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; ( f is isomorphic iff ( f is monotone & ex g being monotone Function of T,S st
( f * g = id T & g * f = id S ) ) )
assume A4:
f is monotone
; ( 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
; f is isomorphic
A7:
f is V7()
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; verum