set f = 0 .--> 0;
set S = Necklace 1;
set T = ComplRelStr (Necklace 1);
A1: the carrier of (Necklace 1) = the carrier of (ComplRelStr (Necklace 1)) by Def8;
A2: the carrier of (Necklace 1) = {0} by Th19, CARD_1:49;
then ( dom (0 .--> 0) = the carrier of (Necklace 1) & rng (0 .--> 0) c= the carrier of (ComplRelStr (Necklace 1)) ) by A1, FUNCOP_1:13;
then 0 .--> 0 is Relation of the carrier of (Necklace 1), the carrier of (ComplRelStr (Necklace 1)) by RELSET_1:4;
then reconsider g = 0 .--> 0 as Function of (Necklace 1),(ComplRelStr (Necklace 1)) by A2;
A3: rng g = {0} 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:
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:
A8: x = 0 by A6, TARSKI:def 1;
y = 0 by A7;
hence ( y in rng g & x = g . y ) by A3, A8, TARSKI:def 1; :: thesis:

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:
A11: y = 0 by A3, A9, TARSKI:def 1;
x = 0 by A10;
hence ( x in dom g & y = g . x ) by A11, TARSKI:def 1; :: thesis:

end;

hence ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) ) by A3, A5; :: thesis:

end;

then reconsider h = g " as Function of (ComplRelStr (Necklace 1)),(Necklace 1) by A1, A3, FUNCT_1:32;
A12: h is monotone

proof

let x, y be Element of (ComplRelStr (Necklace 1)); :: according to ORDERS_3:def 5 :: thesis:
assume x <= y ; :: thesis:
then [x,y] in the InternalRel of (ComplRelStr (Necklace 1)) by ORDERS_2:def 5;
then [x,y] in ( the InternalRel of (Necklace 1) `) \ (id the carrier of (Necklace 1)) by Def8;
then not [x,y] in id the carrier of (Necklace 1) by XBOOLE_0:def 5;
then A13: ( not x in the carrier of (Necklace 1) or x <> y ) by RELAT_1:def 10;
let a, b be Element of (Necklace 1); :: thesis:
assume that
a = h . x and
b = h . y ; :: thesis:
A14: x in the carrier of (ComplRelStr (Necklace 1)) ;
A15: the carrier of (ComplRelStr (Necklace 1)) = Segm 1 by A1, Th19;
then ( x in Segm 1 & y in Segm 1 ) ;
then reconsider i = x, j = y as Nat ;
A16: j = 0 by A15, CARD_1:49, TARSKI:def 1;
A17: i = 0 by A15, CARD_1:49, TARSKI:def 1;
A18: ( i + 1 <> j & j + 1 <> i & i <> j )

proof

hereby :: thesis:

assume A19: ( i + 1 = j or j + 1 = i ) ; :: thesis:

per cases by A19;

suppose i + 1 = j ; :: thesis:

hence contradiction by A15, A17, NAT_1:44; :: thesis:

end;

suppose j + 1 = i ; :: thesis:

hence contradiction by A15, A16, NAT_1:44; :: thesis:

end;

end;

end;

thus i <> j by A13, A14, Def8; :: thesis:

end;

A20: y = 0 by A15, CARD_1:49, TARSKI:def 1;
the carrier of (ComplRelStr (Necklace 1)) = {0} by A1, Th19, CARD_1:49;
hence a <= b by A18, A20, TARSKI:def 1; :: thesis:

end;

g is monotone

proof

let x, y be Element of (Necklace 1); :: according to ORDERS_3:def 5 :: thesis:
assume x <= y ; :: thesis:
then A21: [x,y] in the InternalRel of (Necklace 1) by ORDERS_2:def 5;
the carrier of (Necklace 1) = 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 (ComplRelStr (Necklace 1)); :: thesis:
assume that
a = g . x and
b = g . y ; :: thesis:
the carrier of (Necklace 1) = {0} by Th19, CARD_1:49;
then A22: ( x = 0 & y = 0 ) by TARSKI:def 1;
( i = j + 1 or j = i + 1 ) by A21, Th23;
hence a <= b by A22; :: thesis:

end;

then g is isomorphic by A12, WAYBEL_0:def 38;
hence Necklace 1, ComplRelStr (Necklace 1) are_isomorphic ; :: thesis: