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

A12: h is monotone

hence Necklace 1, ComplRelStr (Necklace 1) are_isomorphic ; :: thesis: verum

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

then reconsider h = g " as Function of (ComplRelStr (Necklace 1)),(Necklace 1) by A1, A3, FUNCT_1:32;
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 ) )

end;A5: ( x in dom g & y = g . x implies ( y in rng g & x = g . y ) )

proof

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

A6: x in dom g and

A7: y = g . x ; :: thesis: ( y in rng g & x = g . y )

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

end;A6: x in dom g and

A7: y = g . x ; :: thesis: ( y in rng g & x = g . y )

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

proof

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

A9: y in rng g and

A10: x = g . y ; :: thesis: ( x in dom g & y = g . x )

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

end;A9: y in rng g and

A10: x = g . y ; :: thesis: ( x in dom g & y = g . x )

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

A12: h is monotone

proof

g is monotone
let x, y be Element of (ComplRelStr (Necklace 1)); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b_{1}, b_{2} being Element of the carrier of (Necklace 1) holds

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

assume x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of (Necklace 1) holds

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

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

the carrier of (ComplRelStr (Necklace 1)) = {0} by A1, Th19, CARD_1:49;

hence a <= b by A18, A20, TARSKI:def 1; :: thesis: verum

end;( not b

assume x <= y ; :: thesis: for b

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

end;

A20:
y = 0
by A15, CARD_1:49, TARSKI:def 1;hereby :: thesis: i <> j

thus
i <> j
by A13, A14, Def8; :: thesis: verumassume A19:
( i + 1 = j or j + 1 = i )
; :: thesis: contradiction

end;the carrier of (ComplRelStr (Necklace 1)) = {0} by A1, Th19, CARD_1:49;

hence a <= b by A18, A20, TARSKI:def 1; :: thesis: verum

proof

then
g is isomorphic
by A12, WAYBEL_0:def 38;
let x, y be Element of (Necklace 1); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b_{1}, b_{2} being Element of the carrier of (ComplRelStr (Necklace 1)) holds

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

assume x <= y ; :: thesis: for b_{1}, b_{2} being Element of the carrier of (ComplRelStr (Necklace 1)) holds

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

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: ( 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 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: verum

end;( not b

assume x <= y ; :: thesis: for b

( not b

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: ( 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 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: verum

hence Necklace 1, ComplRelStr (Necklace 1) are_isomorphic ; :: thesis: verum