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 ) )
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));
ORDERS_3:def 5 ( not x <= y or for b1, b2 being Element of the carrier of (Necklace 1) holds
( not b1 = h . x or not b2 = h . y or b1 <= b2 ) )
assume
x <= y
;
for b1, b2 being Element of the carrier of (Necklace 1) holds
( not b1 = h . x or not b2 = h . y or b1 <= b2 )
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);
( not a = h . x or not b = h . y or a <= b )
assume that
a = h . x
and
b = h . y
;
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
hereby i <> j
assume A19:
(
i + 1
= j or
j + 1
= i )
;
contradiction
end;
thus
i <> j
by A13, A14, Def8;
verum
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;
verum
end;
g is monotone
then
g is isomorphic
by A12, WAYBEL_0:def 38;
hence
Necklace 1, ComplRelStr (Necklace 1) are_isomorphic
; verum