set S = Necklace 1;
set T = ComplRelStr (Necklace 1);
set f = 0 .--> 0 ;
A2: the carrier of (Necklace 1) = {0 } by Th21, CARD_1:87;
A3: the carrier of (Necklace 1) = the carrier of (ComplRelStr (Necklace 1)) by Def9;
then reconsider g = 0 .--> 0 as Function of (Necklace 1),(ComplRelStr (Necklace 1)) by A2;
A4: dom g = {0 } by FUNCOP_1:19;
A5: rng g = {0 } by FUNCOP_1:14;
A6: g is monotone

proof

let x, y be Element of (Necklace 1); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of (ComplRelStr (Necklace 1)) holds
( not b₁ = g . x or not b₂ = g . y or b₁ <= b₂ ) )
assume A7: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of (ComplRelStr (Necklace 1)) holds
( not b₁ = g . x or not b₂ = g . y or b₁ <= b₂ )
the carrier of (Necklace 1) = 1 by Th21;
then reconsider i = x, j = y as Nat by Th4;
[x,y] in the InternalRel of (Necklace 1) by A7, ORDERS_2:def 9;
then A8: ( i = j + 1 or j = i + 1 ) by Th25;
let a, b be Element of (ComplRelStr (Necklace 1)); :: thesis: ( not a = g . x or not b = g . y or a <= b )
assume ( a = g . x & b = g . y ) ; :: thesis: a <= b
A9: the carrier of (Necklace 1) = {0 } by Th21, CARD_1:87;
then A10: x = 0 by TARSKI:def 1;
y = 0 by A9, TARSKI:def 1;
hence a <= b by A8, A10; :: thesis: verum

end;

g = g "

proof

for y, x being set holds
( y in rng g & x = g . y iff ( x in dom g & y = g . x ) )

proof

let x, y be set ; :: thesis: ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) )
A11: ( y in rng g & x = g . y implies ( x in dom g & y = g . x ) )

proof

assume that
A12: y in rng g and
A13: x = g . y ; :: thesis: ( x in dom g & y = g . x )
A14: y = 0 by A5, A12, TARSKI:def 1;
then x = 0 by A13, FUNCOP_1:87;
hence ( x in dom g & y = g . x ) by A4, A14, FUNCOP_1:87, TARSKI:def 1; :: thesis: verum

end;

( x in dom g & y = g . x implies ( y in rng g & x = g . y ) )

proof

assume that
A15: x in dom g and
A16: y = g . x ; :: thesis: ( y in rng g & x = g . y )
the carrier of (Necklace 1) = {0 } by Th21, CARD_1:87;
then A17: x = 0 by A15, TARSKI:def 1;
then y = 0 by A16, FUNCOP_1:87;
hence ( y in rng g & x = g . y ) by A5, A17, FUNCOP_1:87, TARSKI:def 1; :: thesis: verum

end;

hence ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) ) by A5, A11, FUNCOP_1:19; :: thesis: verum

end;

hence g = g " by A4, A5, FUNCT_1:54; :: thesis: verum

end;

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

proof

let x, y be Element of (ComplRelStr (Necklace 1)); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b₁, b₂ being Element of the carrier of (Necklace 1) holds
( not b₁ = h . x or not b₂ = h . y or b₁ <= b₂ ) )
assume A18: x <= y ; :: thesis: for b₁, b₂ being Element of the carrier of (Necklace 1) holds
( not b₁ = h . x or not b₂ = h . y or b₁ <= b₂ )
A19: the carrier of (ComplRelStr (Necklace 1)) = 1 by A3, Th21;
then reconsider i = x, j = y as Nat by Th4;
[x,y] in the InternalRel of (ComplRelStr (Necklace 1)) by A18, ORDERS_2:def 9;
then [x,y] in (the InternalRel of (Necklace 1) ` ) \ (id the carrier of (Necklace 1)) by Def9;
then not [x,y] in id the carrier of (Necklace 1) by XBOOLE_0:def 5;
then A20: ( not x in the carrier of (Necklace 1) or x <> y ) by RELAT_1:def 10;
A21: ( x in the carrier of (ComplRelStr (Necklace 1)) & y in the carrier of (ComplRelStr (Necklace 1)) ) ;
A22: i = 0 by A19, CARD_1:87, TARSKI:def 1;
A23: j = 0 by A19, CARD_1:87, TARSKI:def 1;
A24: ( i + 1 <> j & j + 1 <> i & i <> j )

proof

hereby :: thesis: i <> j

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

per cases ( i + 1 = j or j + 1 = i ) by A25;

suppose i + 1 = j ; :: thesis: contradiction

hence contradiction by A19, A22, NAT_1:45; :: thesis: verum

end;

suppose j + 1 = i ; :: thesis: contradiction

hence contradiction by A19, A23, NAT_1:45; :: thesis: verum

end;

end;

end;

thus i <> j by A20, A21, Def9; :: thesis: verum

end;

let a, b be Element of (Necklace 1); :: thesis: ( not a = h . x or not b = h . y or a <= b )
assume ( a = h . x & b = h . y ) ; :: thesis: a <= b
A26: the carrier of (ComplRelStr (Necklace 1)) = {0 } by A3, Th21, CARD_1:87;
y = 0 by A19, CARD_1:87, TARSKI:def 1;
hence a <= b by A24, A26, TARSKI:def 1; :: thesis: verum

end;

then g is isomorphic by A6, WAYBEL_0:def 38;
hence Necklace 1, ComplRelStr (Necklace 1) are_isomorphic by WAYBEL_1:def 8; :: thesis: verum