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 Def9;
the carrier of (Necklace 1) = {0} by Th21, CARD_1:49;
then reconsider g = 0 .--> 0 as Function of (Necklace 1),(ComplRelStr (Necklace 1)) by Def9;
A2: rng g = {0} by FUNCOP_1:8;
A3: dom g = {0} by FUNCOP_1:13;
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 ) )
A4: ( x in dom g & y = g . x implies ( y in rng g & x = g . y ) )

proof

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

end;

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

proof

assume that
A8: y in rng g and
A9: x = g . y ; :: thesis: ( x in dom g & y = g . x )
A10: y = 0 by A2, A8, TARSKI:def 1;
then x = 0 by A9, FUNCOP_1:72;
hence ( x in dom g & y = g . x ) by A3, A10, FUNCOP_1:72, TARSKI:def 1; :: thesis: verum

end;

hence ( x in rng g & y = g . x iff ( y in dom g & x = g . y ) ) by A2, A4, FUNCOP_1:13; :: thesis: verum

end;

then reconsider h = g " as Function of (ComplRelStr (Necklace 1)),(Necklace 1) by A1, A3, A2, FUNCT_1:32;
A11: 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 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₂ )
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 Def9;
then not [x,y] in id the carrier of (Necklace 1) by XBOOLE_0:def 5;
then A12: ( 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: ( not a = h . x or not b = h . y or a <= b )
assume that
a = h . x and
b = h . y ; :: thesis: a <= b
A13: x in the carrier of (ComplRelStr (Necklace 1)) ;
A14: the carrier of (ComplRelStr (Necklace 1)) = 1 by A1, Th21;
then reconsider i = x, j = y as Nat by Th4;
A15: j = 0 by A14, CARD_1:49, TARSKI:def 1;
A16: i = 0 by A14, CARD_1:49, TARSKI:def 1;
A17: ( i + 1 <> j & j + 1 <> i & i <> j )

proof

hereby :: thesis: i <> j

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

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

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

hence contradiction by A14, A16, NAT_1:44; :: thesis: verum

end;

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

hence contradiction by A14, A15, NAT_1:44; :: thesis: verum

end;

end;

end;

thus i <> j by A12, A13, Def9; :: thesis: verum

end;

A19: y = 0 by A14, CARD_1:49, TARSKI:def 1;
the carrier of (ComplRelStr (Necklace 1)) = {0} by A1, Th21, CARD_1:49;
hence a <= b by A17, A19, TARSKI:def 1; :: thesis: verum

end;

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 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₂ )
then A20: [x,y] in the InternalRel of (Necklace 1) by ORDERS_2:def 5;
the carrier of (Necklace 1) = 1 by Th21;
then reconsider i = x, j = y as Nat by Th4;
let a, b be Element of (ComplRelStr (Necklace 1)); :: 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 (Necklace 1) = {0} by Th21, CARD_1:49;
then A21: ( x = 0 & y = 0 ) by TARSKI:def 1;
( i = j + 1 or j = i + 1 ) by A20, Th25;
hence a <= b by A21; :: thesis: verum

end;

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