let S, T be non empty RelStr ; :: thesis: for f being Function of S,T holds
( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )
let f be Function of S,T; :: thesis: ( f is isomorphic iff ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) ) )

hereby :: thesis: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ) implies f is isomorphic )

assume A1: f is isomorphic ; :: thesis: ( f is one-to-one & rng f = the carrier of T & ( for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) )
hence f is one-to-one by Def38; :: thesis: ( rng f = the carrier of T & ( for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) ) ) )
consider g being Function of T,S such that
A2: g = f " and
A3: g is monotone by A1, Def38;
A4: ( f is one-to-one & f is monotone ) by A1, Def38;
then rng f = dom g by A2, FUNCT_1:33;
hence rng f = the carrier of T by FUNCT_2:def 1; :: thesis: for x, y being Element of S holds
( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
let x, y be Element of S; :: thesis: ( ( x <= y implies f . x <= f . y ) & ( f . x <= f . y implies x <= y ) )
thus ( x <= y implies f . x <= f . y ) by A4; :: thesis: ( f . x <= f . y implies x <= y )
assume A5: f . x <= f . y ; :: thesis: x <= y
A6: g . (f . x) = x by A2, A4, FUNCT_2:26;
g . (f . y) = y by A2, A4, FUNCT_2:26;
hence x <= y by A3, A5, A6; :: thesis: verum

end;

assume that
A7: f is one-to-one and
A8: rng f = the carrier of T and
A9: for x, y being Element of S holds
( x <= y iff f . x <= f . y ) ; :: thesis: f is isomorphic

per cases ( ( not S is empty & not T is empty ) or S is empty or T is empty ) ;
:: according to WAYBEL_0:def 38

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

thus f is one-to-one by A7; :: thesis: ( f is monotone & ex g being Function of T,S st
( g = f " & g is monotone ) )
thus for x, y being Element of S st x <= y holds
for a, b being Element of T st a = f . x & b = f . y holds
a <= b by A9; :: according to ORDERS_3:def 5 :: thesis: ex g being Function of T,S st
( g = f " & g is monotone )
reconsider g = f " as Function of T,S by A7, A8, FUNCT_2:25;
take g ; :: thesis: ( g = f " & g is monotone )
thus g = f " ; :: thesis: g is monotone
let x, y be Element of T; :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of S holds
( not b₁ = g . x or not b₂ = g . y or b₁ <= b₂ ) )
consider a being object such that
A10: a in dom f and
A11: x = f . a by A8, FUNCT_1:def 3;
consider b being object such that
A12: b in dom f and
A13: y = f . b by A8, FUNCT_1:def 3;
reconsider a = a, b = b as Element of S by A10, A12;
A14: g . x = a by A7, A11, FUNCT_2:26;
g . y = b by A7, A13, FUNCT_2:26;
hence ( not x <= y or for b₁, b₂ being Element of the carrier of S holds
( not b₁ = g . x or not b₂ = g . y or b₁ <= b₂ ) ) by A9, A11, A13, A14; :: thesis: verum

end;

case ( S is empty or T is empty ) ; :: thesis: ( S is empty & T is empty )

hence ( S is empty & T is empty ) ; :: thesis: verum

end;

end;