set f = 0 .--> 0;
set S = Necklace 1;
set T = ComplRelStr ();
A1: the carrier of () = the carrier of () by Def8;
A2: the carrier of () = by ;
then ( dom () = the carrier of () & rng () c= the carrier of () ) by ;
then 0 .--> 0 is Relation of the carrier of (), the carrier of () by RELSET_1:4;
then reconsider g = 0 .--> 0 as Function of (),() by A2;
A3: rng g = by FUNCOP_1:8;
for y, x being object holds
( y in rng g & x = g . y iff ( x in dom g & y = g . x ) )
proof
let x, y be object ; :: thesis: ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) )
A5: ( x in dom g & y = g . x implies ( y in rng g & x = g . y ) )
proof
assume that
A6: x in dom g and
A7: y = g . x ; :: thesis: ( y in rng g & x = g . y )
A8: x = 0 by ;
y = 0 by A7;
hence ( y in rng g & x = g . y ) by ; :: thesis: verum
end;
( y in rng g & x = g . y implies ( x in dom g & y = g . x ) )
proof
assume that
A9: y in rng g and
A10: x = g . y ; :: thesis: ( x in dom g & y = g . x )
A11: y = 0 by ;
x = 0 by A10;
hence ( x in dom g & y = g . x ) by ; :: thesis: verum
end;
hence ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) ) by A3, A5; :: thesis: verum
end;
then reconsider h = g " as Function of (),() by ;
A12: h is monotone
proof
let x, y be Element of (); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of () holds
( not b1 = h . x or not b2 = h . y or b1 <= b2 ) )

assume x <= y ; :: thesis: for b1, b2 being Element of the carrier of () holds
( not b1 = h . x or not b2 = h . y or b1 <= b2 )

then [x,y] in the InternalRel of () by ORDERS_2:def 5;
then [x,y] in ( the InternalRel of () `) \ (id the carrier of ()) by Def8;
then not [x,y] in id the carrier of () by XBOOLE_0:def 5;
then A13: ( not x in the carrier of () or x <> y ) by RELAT_1:def 10;
let a, b be Element of (); :: thesis: ( not a = h . x or not b = h . y or a <= b )
assume that
a = h . x and
b = h . y ; :: thesis: a <= b
A14: x in the carrier of () ;
A15: the carrier of () = Segm 1 by ;
then ( x in Segm 1 & y in Segm 1 ) ;
then reconsider i = x, j = y as Nat ;
A16: j = 0 by ;
A17: i = 0 by ;
A18: ( i + 1 <> j & j + 1 <> i & i <> j )
proof
hereby :: thesis: i <> j
assume A19: ( i + 1 = j or j + 1 = i ) ; :: thesis: contradiction
per cases ( i + 1 = j or j + 1 = i ) by A19;
end;
end;
thus i <> j by ; :: thesis: verum
end;
A20: y = 0 by ;
the carrier of () = by ;
hence a <= b by ; :: thesis: verum
end;
g is monotone
proof
let x, y be Element of (); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of () holds
( not b1 = g . x or not b2 = g . y or b1 <= b2 ) )

assume x <= y ; :: thesis: for b1, b2 being Element of the carrier of () holds
( not b1 = g . x or not b2 = g . y or b1 <= b2 )

then A21: [x,y] in the InternalRel of () by ORDERS_2:def 5;
the carrier of () = Segm 1 by Th19;
then ( x in Segm 1 & y in Segm 1 ) ;
then reconsider i = x, j = y as Nat ;
let a, b be Element of (); :: thesis: ( not a = g . x or not b = g . y or a <= b )
assume that
a = g . x and
b = g . y ; :: thesis: a <= b
the carrier of () = by ;
then A22: ( x = 0 & y = 0 ) by TARSKI:def 1;
( i = j + 1 or j = i + 1 ) by ;
hence a <= b by A22; :: thesis: verum
end;
then g is isomorphic by ;
hence Necklace 1, ComplRelStr () are_isomorphic ; :: thesis: verum