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 ) ) ) )

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

( 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 that ( 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;( ( 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

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 38end;

:: 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 ) )

( 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_{1}, b_{2} being Element of the carrier of S holds

( not b_{1} = g . x or not b_{2} = g . y or b_{1} <= b_{2} ) )

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_{1}, b_{2} being Element of the carrier of S holds

( not b_{1} = g . x or not b_{2} = g . y or b_{1} <= b_{2} ) )
by A9, A11, A13, A14; :: thesis: verum

end;( 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

( not 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

( not b