set g = (0,1) --> (1,3);

set h = (2,3) --> (0,2);

set f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2));

set S = Necklace 4;

set T = ComplRelStr (Necklace 4);

A1: rng ((2,3) --> (0,2)) = {0,2} by FUNCT_4:64;

A2: rng ((0,1) --> (1,3)) = {1,3} by FUNCT_4:64;

A3: rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) c= the carrier of (ComplRelStr (Necklace 4))

.= {0,1} \/ (dom ((2,3) --> (0,2))) by FUNCT_4:62

.= {0,1} \/ {2,3} by FUNCT_4:62

.= {0,1,2,3} by ENUMSET1:5 ;

then A7: dom (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) = the carrier of (Necklace 4) by Th19, CARD_1:52;

then reconsider f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2)) as Function of (Necklace 4),(ComplRelStr (Necklace 4)) by A3, FUNCT_2:def 1, RELSET_1:4;

take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic

set h = (2,3) --> (0,2);

set f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2));

set S = Necklace 4;

set T = ComplRelStr (Necklace 4);

A1: rng ((2,3) --> (0,2)) = {0,2} by FUNCT_4:64;

A2: rng ((0,1) --> (1,3)) = {1,3} by FUNCT_4:64;

A3: rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) c= the carrier of (ComplRelStr (Necklace 4))

proof

A6: dom (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) =
(dom ((0,1) --> (1,3))) \/ (dom ((2,3) --> (0,2)))
by FUNCT_4:def 1
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) or x in the carrier of (ComplRelStr (Necklace 4)) )

assume A4: x in rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) ; :: thesis: x in the carrier of (ComplRelStr (Necklace 4))

A5: rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) c= (rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) by FUNCT_4:17;

(rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) = {1,3,0,2} by A2, A1, ENUMSET1:5

.= {0,1,2,3} by ENUMSET1:69 ;

then x in 4 by A4, A5, CARD_1:52;

then x in the carrier of (Necklace 4) by Th19;

hence x in the carrier of (ComplRelStr (Necklace 4)) by Def8; :: thesis: verum

end;assume A4: x in rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) ; :: thesis: x in the carrier of (ComplRelStr (Necklace 4))

A5: rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) c= (rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) by FUNCT_4:17;

(rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) = {1,3,0,2} by A2, A1, ENUMSET1:5

.= {0,1,2,3} by ENUMSET1:69 ;

then x in 4 by A4, A5, CARD_1:52;

then x in the carrier of (Necklace 4) by Th19;

hence x in the carrier of (ComplRelStr (Necklace 4)) by Def8; :: thesis: verum

.= {0,1} \/ (dom ((2,3) --> (0,2))) by FUNCT_4:62

.= {0,1} \/ {2,3} by FUNCT_4:62

.= {0,1,2,3} by ENUMSET1:5 ;

then A7: dom (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) = the carrier of (Necklace 4) by Th19, CARD_1:52;

then reconsider f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2)) as Function of (Necklace 4),(ComplRelStr (Necklace 4)) by A3, FUNCT_2:def 1, RELSET_1:4;

take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic

per cases
( ( not Necklace 4 is empty & not ComplRelStr (Necklace 4) is empty ) or Necklace 4 is empty or ComplRelStr (Necklace 4) is empty )
;

:: according to WAYBEL_0:def 38end;

:: according to WAYBEL_0:def 38

case that
not Necklace 4 is empty
and

not ComplRelStr (Necklace 4) is empty ; :: thesis: ( f is one-to-one & f is monotone & ex b_{1} being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st

( b_{1} = f " & b_{1} is monotone ) )

not ComplRelStr (Necklace 4) is empty ; :: thesis: ( f is one-to-one & f is monotone & ex b

( b

set A = the InternalRel of (ComplRelStr (Necklace 4));

A8: rng (0 .--> 1) misses rng (1 .--> 3)

A14: rng (2 .--> 0) misses rng (3 .--> 2)

then A17: (2,3) --> (0,2) is one-to-one by A14, FUNCT_4:92;

A18: dom ((0,1) --> (1,3)) misses dom ((2,3) --> (0,2))

.= {1,3,0,2} by A2, A1, ENUMSET1:5

.= {0,1,2,3} by ENUMSET1:69

.= the carrier of (Necklace 4) by Th19, CARD_1:52

.= the carrier of (ComplRelStr (Necklace 4)) by Def8 ;

(0,1) --> (1,3) = (0 .--> 1) +* (1 .--> 3) by FUNCT_4:def 4;

then A22: (0,1) --> (1,3) is one-to-one by A8, FUNCT_4:92;

hence f is V7() by A17, A11, FUNCT_4:92; :: thesis: ( f is monotone & ex b_{1} being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st

( b_{1} = f " & b_{1} is monotone ) )

then reconsider F = f " as Function of (ComplRelStr (Necklace 4)),(Necklace 4) by A21, FUNCT_2:25;

A23: {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} c= the InternalRel of (ComplRelStr (Necklace 4))_{1} being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st

( b_{1} = f " & b_{1} is monotone )

thus F = f " ; :: thesis: F is monotone

thus F is monotone :: thesis: verum

end;A8: rng (0 .--> 1) misses rng (1 .--> 3)

proof

A11:
rng ((0,1) --> (1,3)) misses rng ((2,3) --> (0,2))
assume
rng (0 .--> 1) meets rng (1 .--> 3)
; :: thesis: contradiction

then consider x being object such that

A9: x in rng (0 .--> 1) and

A10: x in rng (1 .--> 3) by XBOOLE_0:3;

rng (0 .--> 1) = {1} by FUNCOP_1:8;

then ( rng (1 .--> 3) = {3} & x = 1 ) by A9, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A10, TARSKI:def 1; :: thesis: verum

end;then consider x being object such that

A9: x in rng (0 .--> 1) and

A10: x in rng (1 .--> 3) by XBOOLE_0:3;

rng (0 .--> 1) = {1} by FUNCOP_1:8;

then ( rng (1 .--> 3) = {3} & x = 1 ) by A9, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A10, TARSKI:def 1; :: thesis: verum

proof

set B = {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]};
assume
rng ((0,1) --> (1,3)) meets rng ((2,3) --> (0,2))
; :: thesis: contradiction

then consider x being object such that

A12: x in rng ((0,1) --> (1,3)) and

A13: x in rng ((2,3) --> (0,2)) by XBOOLE_0:3;

( x = 1 or x = 3 ) by A2, A12, TARSKI:def 2;

hence contradiction by A1, A13, TARSKI:def 2; :: thesis: verum

end;then consider x being object such that

A12: x in rng ((0,1) --> (1,3)) and

A13: x in rng ((2,3) --> (0,2)) by XBOOLE_0:3;

( x = 1 or x = 3 ) by A2, A12, TARSKI:def 2;

hence contradiction by A1, A13, TARSKI:def 2; :: thesis: verum

A14: rng (2 .--> 0) misses rng (3 .--> 2)

proof

(2,3) --> (0,2) = (2 .--> 0) +* (3 .--> 2)
by FUNCT_4:def 4;
assume
rng (2 .--> 0) meets rng (3 .--> 2)
; :: thesis: contradiction

then consider x being object such that

A15: x in rng (2 .--> 0) and

A16: x in rng (3 .--> 2) by XBOOLE_0:3;

rng (2 .--> 0) = {0} by FUNCOP_1:8;

then ( rng (3 .--> 2) = {2} & x = 0 ) by A15, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A16, TARSKI:def 1; :: thesis: verum

end;then consider x being object such that

A15: x in rng (2 .--> 0) and

A16: x in rng (3 .--> 2) by XBOOLE_0:3;

rng (2 .--> 0) = {0} by FUNCOP_1:8;

then ( rng (3 .--> 2) = {2} & x = 0 ) by A15, FUNCOP_1:8, TARSKI:def 1;

hence contradiction by A16, TARSKI:def 1; :: thesis: verum

then A17: (2,3) --> (0,2) is one-to-one by A14, FUNCT_4:92;

A18: dom ((0,1) --> (1,3)) misses dom ((2,3) --> (0,2))

proof

then A21: rng f =
(rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2)))
by FRECHET:35, PARTFUN1:56
assume
dom ((0,1) --> (1,3)) meets dom ((2,3) --> (0,2))
; :: thesis: contradiction

then consider x being object such that

A19: x in dom ((0,1) --> (1,3)) and

A20: x in dom ((2,3) --> (0,2)) by XBOOLE_0:3;

( x = 0 or x = 1 ) by A19, TARSKI:def 2;

hence contradiction by A20, TARSKI:def 2; :: thesis: verum

end;then consider x being object such that

A19: x in dom ((0,1) --> (1,3)) and

A20: x in dom ((2,3) --> (0,2)) by XBOOLE_0:3;

( x = 0 or x = 1 ) by A19, TARSKI:def 2;

hence contradiction by A20, TARSKI:def 2; :: thesis: verum

.= {1,3,0,2} by A2, A1, ENUMSET1:5

.= {0,1,2,3} by ENUMSET1:69

.= the carrier of (Necklace 4) by Th19, CARD_1:52

.= the carrier of (ComplRelStr (Necklace 4)) by Def8 ;

(0,1) --> (1,3) = (0 .--> 1) +* (1 .--> 3) by FUNCT_4:def 4;

then A22: (0,1) --> (1,3) is one-to-one by A8, FUNCT_4:92;

hence f is V7() by A17, A11, FUNCT_4:92; :: thesis: ( f is monotone & ex b

( b

then reconsider F = f " as Function of (ComplRelStr (Necklace 4)),(Necklace 4) by A21, FUNCT_2:25;

A23: {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} c= the InternalRel of (ComplRelStr (Necklace 4))

proof

thus
f is monotone
:: thesis: ex b
set C = the carrier of (Necklace 4);

let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} or x in the InternalRel of (ComplRelStr (Necklace 4)) )

assume x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} ; :: thesis: x in the InternalRel of (ComplRelStr (Necklace 4))

then A24: ( x = [1,3] or x = [3,1] or x = [0,2] or x = [2,0] or x = [0,3] or x = [3,0] ) by ENUMSET1:def 4;

A25: ( 2 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A6, A7, ENUMSET1:def 2;

( 0 in the carrier of (Necklace 4) & 1 in the carrier of (Necklace 4) ) by A6, A7, ENUMSET1:def 2;

then reconsider x9 = x as Element of [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A24, A25, ZFMISC_1:87;

not x9 in the InternalRel of (Necklace 4)

not x in id the carrier of (Necklace 4) by A24, RELAT_1:def 10;

then x in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A27, XBOOLE_0:def 5;

hence x in the InternalRel of (ComplRelStr (Necklace 4)) by Def8; :: thesis: verum

end;let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} or x in the InternalRel of (ComplRelStr (Necklace 4)) )

assume x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} ; :: thesis: x in the InternalRel of (ComplRelStr (Necklace 4))

then A24: ( x = [1,3] or x = [3,1] or x = [0,2] or x = [2,0] or x = [0,3] or x = [3,0] ) by ENUMSET1:def 4;

A25: ( 2 in the carrier of (Necklace 4) & 3 in the carrier of (Necklace 4) ) by A6, A7, ENUMSET1:def 2;

( 0 in the carrier of (Necklace 4) & 1 in the carrier of (Necklace 4) ) by A6, A7, ENUMSET1:def 2;

then reconsider x9 = x as Element of [: the carrier of (Necklace 4), the carrier of (Necklace 4):] by A24, A25, ZFMISC_1:87;

not x9 in the InternalRel of (Necklace 4)

proof

then A27:
x9 in the InternalRel of (Necklace 4) `
by SUBSET_1:29;
assume
x9 in the InternalRel of (Necklace 4)
; :: thesis: contradiction

then consider i being Element of NAT such that

i + 1 < 4 and

A26: ( x9 = [i,(i + 1)] or x9 = [(i + 1),i] ) by Th18;

( ( i = 1 & i + 1 = 3 ) or ( i = 3 & i + 1 = 1 ) or ( i = 0 & i + 1 = 2 ) or ( i = 2 & i + 1 = 0 ) or ( i = 0 & i + 1 = 3 ) or ( i = 3 & i + 1 = 0 ) ) by A24, A26, XTUPLE_0:1;

hence contradiction ; :: thesis: verum

end;then consider i being Element of NAT such that

i + 1 < 4 and

A26: ( x9 = [i,(i + 1)] or x9 = [(i + 1),i] ) by Th18;

( ( i = 1 & i + 1 = 3 ) or ( i = 3 & i + 1 = 1 ) or ( i = 0 & i + 1 = 2 ) or ( i = 2 & i + 1 = 0 ) or ( i = 0 & i + 1 = 3 ) or ( i = 3 & i + 1 = 0 ) ) by A24, A26, XTUPLE_0:1;

hence contradiction ; :: thesis: verum

not x in id the carrier of (Necklace 4) by A24, RELAT_1:def 10;

then x in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by A27, XBOOLE_0:def 5;

hence x in the InternalRel of (ComplRelStr (Necklace 4)) by Def8; :: thesis: verum

( b

proof

take
F
; :: thesis: ( F = f " & F is monotone )
A28:
dom ((2,3) --> (0,2)) = {2,3}
by FUNCT_4:62;

then 2 in dom ((2,3) --> (0,2)) by TARSKI:def 2;

then A29: f . 2 = ((2,3) --> (0,2)) . 2 by FUNCT_4:13

.= 0 by FUNCT_4:63 ;

3 in dom ((2,3) --> (0,2)) by A28, TARSKI:def 2;

then A30: f . 3 = ((2,3) --> (0,2)) . 3 by FUNCT_4:13

.= 2 by FUNCT_4:63 ;

A31: dom ((0,1) --> (1,3)) = {0,1} by FUNCT_4:62;

then 0 in dom ((0,1) --> (1,3)) by TARSKI:def 2;

then A32: f . 0 = ((0,1) --> (1,3)) . 0 by A18, FUNCT_4:16

.= 1 by FUNCT_4:63 ;

1 in dom ((0,1) --> (1,3)) by A31, TARSKI:def 2;

then A33: f . 1 = ((0,1) --> (1,3)) . 1 by A18, FUNCT_4:16

.= 3 by FUNCT_4:63 ;

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

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

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

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

then A34: [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def 5;

the carrier of (Necklace 4) = 4 by Th19;

then ( x in Segm 4 & y in Segm 4 ) ;

then reconsider i = x, j = y as Nat ;

A35: ( i = j + 1 or j = i + 1 ) by A34, Th23;

let a, b be Element of (ComplRelStr (Necklace 4)); :: thesis: ( not a = f . x or not b = f . y or a <= b )

assume A36: ( a = f . x & b = f . y ) ; :: thesis: a <= b

end;then 2 in dom ((2,3) --> (0,2)) by TARSKI:def 2;

then A29: f . 2 = ((2,3) --> (0,2)) . 2 by FUNCT_4:13

.= 0 by FUNCT_4:63 ;

3 in dom ((2,3) --> (0,2)) by A28, TARSKI:def 2;

then A30: f . 3 = ((2,3) --> (0,2)) . 3 by FUNCT_4:13

.= 2 by FUNCT_4:63 ;

A31: dom ((0,1) --> (1,3)) = {0,1} by FUNCT_4:62;

then 0 in dom ((0,1) --> (1,3)) by TARSKI:def 2;

then A32: f . 0 = ((0,1) --> (1,3)) . 0 by A18, FUNCT_4:16

.= 1 by FUNCT_4:63 ;

1 in dom ((0,1) --> (1,3)) by A31, TARSKI:def 2;

then A33: f . 1 = ((0,1) --> (1,3)) . 1 by A18, FUNCT_4:16

.= 3 by FUNCT_4:63 ;

let x, y be Element of (Necklace 4); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b

( not b

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

( not b

then A34: [x,y] in the InternalRel of (Necklace 4) by ORDERS_2:def 5;

the carrier of (Necklace 4) = 4 by Th19;

then ( x in Segm 4 & y in Segm 4 ) ;

then reconsider i = x, j = y as Nat ;

A35: ( i = j + 1 or j = i + 1 ) by A34, Th23;

let a, b be Element of (ComplRelStr (Necklace 4)); :: thesis: ( not a = f . x or not b = f . y or a <= b )

assume A36: ( a = f . x & b = f . y ) ; :: thesis: a <= b

per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) )
by A6, A7, ENUMSET1:def 2;

end;

suppose
( x = 0 & y = 1 )
; :: thesis: a <= b

then
[a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]}
by A36, A32, A33, ENUMSET1:def 4;

hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

end;hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

suppose
( x = 1 & y = 0 )
; :: thesis: a <= b

then
[a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]}
by A36, A32, A33, ENUMSET1:def 4;

hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

end;hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

suppose
( x = 1 & y = 2 )
; :: thesis: a <= b

then
[a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]}
by A36, A33, A29, ENUMSET1:def 4;

hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

end;hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

suppose
( x = 2 & y = 1 )
; :: thesis: a <= b

then
[a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]}
by A36, A33, A29, ENUMSET1:def 4;

hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

end;hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

suppose
( x = 2 & y = 3 )
; :: thesis: a <= b

then
[a,b] in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]}
by A36, A29, A30, ENUMSET1:def 4;

hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

end;hence a <= b by A23, ORDERS_2:def 5; :: thesis: verum

thus F = f " ; :: thesis: F is monotone

thus F is monotone :: thesis: verum

proof

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

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

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

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

then [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5;

then A37: [x,y] in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by Def8;

then not [x,y] in id the carrier of (Necklace 4) by XBOOLE_0:def 5;

then A38: ( not x in the carrier of (Necklace 4) or x <> y ) by RELAT_1:def 10;

( [x,y] in the InternalRel of (Necklace 4) ` implies not [x,y] in the InternalRel of (Necklace 4) ) by XBOOLE_0:def 5;

then A39: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } \/ { [(l + 1),l] where l is Element of NAT : l + 1 < 4 } by A37, Th17, XBOOLE_0:def 5;

then A40: not [x,y] in { [(k + 1),k] where k is Element of NAT : k + 1 < 4 } by XBOOLE_0:def 3;

A41: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by Def8

.= Segm 4 by Th19 ;

then ( x in Segm 4 & y in Segm 4 ) ;

then ( x is natural & y is natural ) ;

then reconsider i = x, j = y as Element of NAT by ORDINAL1:def 12;

A42: x in the carrier of (ComplRelStr (Necklace 4)) ;

A43: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } by A39, XBOOLE_0:def 3;

A44: ( i + 1 <> j & j + 1 <> i & i <> j )

then A49: dom (((2,3) --> (0,2)) ") = {0,2} by FUNCT_4:62;

then A50: 0 in dom (((2,3) --> (0,2)) ") by TARSKI:def 2;

A51: F . 0 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 0 by A22, A17, A18, A11, Th6

.= (((2,3) --> (0,2)) ") . 0 by A50, FUNCT_4:13

.= 2 by A48, FUNCT_4:63 ;

A52: ((0,1) --> (1,3)) " = (1,3) --> (0,1) by Th9;

then A53: dom (((0,1) --> (1,3)) ") = {1,3} by FUNCT_4:62;

then A54: 1 in dom (((0,1) --> (1,3)) ") by TARSKI:def 2;

A55: dom (((0,1) --> (1,3)) ") misses dom (((2,3) --> (0,2)) ")

.= (((0,1) --> (1,3)) ") . 1 by A55, A54, FUNCT_4:16

.= 0 by A52, FUNCT_4:63 ;

A59: 2 in dom (((2,3) --> (0,2)) ") by A49, TARSKI:def 2;

A60: F . 2 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 2 by A22, A17, A18, A11, Th6

.= (((2,3) --> (0,2)) ") . 2 by A59, FUNCT_4:13

.= 3 by A48, FUNCT_4:63 ;

A61: 3 in dom (((0,1) --> (1,3)) ") by A53, TARSKI:def 2;

A62: F . 3 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 3 by A22, A17, A18, A11, Th6

.= (((0,1) --> (1,3)) ") . 3 by A55, A61, FUNCT_4:16

.= 1 by A52, FUNCT_4:63 ;

let a, b be Element of (Necklace 4); :: thesis: ( not a = F . x or not b = F . y or a <= b )

assume that

A63: a = F . x and

A64: b = F . y ; :: thesis: a <= b

end;( not b

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

( not b

then [x,y] in the InternalRel of (ComplRelStr (Necklace 4)) by ORDERS_2:def 5;

then A37: [x,y] in ( the InternalRel of (Necklace 4) `) \ (id the carrier of (Necklace 4)) by Def8;

then not [x,y] in id the carrier of (Necklace 4) by XBOOLE_0:def 5;

then A38: ( not x in the carrier of (Necklace 4) or x <> y ) by RELAT_1:def 10;

( [x,y] in the InternalRel of (Necklace 4) ` implies not [x,y] in the InternalRel of (Necklace 4) ) by XBOOLE_0:def 5;

then A39: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } \/ { [(l + 1),l] where l is Element of NAT : l + 1 < 4 } by A37, Th17, XBOOLE_0:def 5;

then A40: not [x,y] in { [(k + 1),k] where k is Element of NAT : k + 1 < 4 } by XBOOLE_0:def 3;

A41: the carrier of (ComplRelStr (Necklace 4)) = the carrier of (Necklace 4) by Def8

.= Segm 4 by Th19 ;

then ( x in Segm 4 & y in Segm 4 ) ;

then ( x is natural & y is natural ) ;

then reconsider i = x, j = y as Element of NAT by ORDINAL1:def 12;

A42: x in the carrier of (ComplRelStr (Necklace 4)) ;

A43: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } by A39, XBOOLE_0:def 3;

A44: ( i + 1 <> j & j + 1 <> i & i <> j )

proof

end;

A48:
((2,3) --> (0,2)) " = (0,2) --> (2,3)
by Th9;hereby :: thesis: i <> j

thus
i <> j
by A38, A42, Def8; :: thesis: verumassume A45:
( i + 1 = j or j + 1 = i )
; :: thesis: contradiction

end;then A49: dom (((2,3) --> (0,2)) ") = {0,2} by FUNCT_4:62;

then A50: 0 in dom (((2,3) --> (0,2)) ") by TARSKI:def 2;

A51: F . 0 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 0 by A22, A17, A18, A11, Th6

.= (((2,3) --> (0,2)) ") . 0 by A50, FUNCT_4:13

.= 2 by A48, FUNCT_4:63 ;

A52: ((0,1) --> (1,3)) " = (1,3) --> (0,1) by Th9;

then A53: dom (((0,1) --> (1,3)) ") = {1,3} by FUNCT_4:62;

then A54: 1 in dom (((0,1) --> (1,3)) ") by TARSKI:def 2;

A55: dom (((0,1) --> (1,3)) ") misses dom (((2,3) --> (0,2)) ")

proof

A58: F . 1 =
((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 1
by A22, A17, A18, A11, Th6
assume
dom (((0,1) --> (1,3)) ") meets dom (((2,3) --> (0,2)) ")
; :: thesis: contradiction

then consider x being object such that

A56: x in dom (((0,1) --> (1,3)) ") and

A57: x in dom (((2,3) --> (0,2)) ") by XBOOLE_0:3;

( x = 1 or x = 3 ) by A53, A56, TARSKI:def 2;

hence contradiction by A49, A57, TARSKI:def 2; :: thesis: verum

end;then consider x being object such that

A56: x in dom (((0,1) --> (1,3)) ") and

A57: x in dom (((2,3) --> (0,2)) ") by XBOOLE_0:3;

( x = 1 or x = 3 ) by A53, A56, TARSKI:def 2;

hence contradiction by A49, A57, TARSKI:def 2; :: thesis: verum

.= (((0,1) --> (1,3)) ") . 1 by A55, A54, FUNCT_4:16

.= 0 by A52, FUNCT_4:63 ;

A59: 2 in dom (((2,3) --> (0,2)) ") by A49, TARSKI:def 2;

A60: F . 2 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 2 by A22, A17, A18, A11, Th6

.= (((2,3) --> (0,2)) ") . 2 by A59, FUNCT_4:13

.= 3 by A48, FUNCT_4:63 ;

A61: 3 in dom (((0,1) --> (1,3)) ") by A53, TARSKI:def 2;

A62: F . 3 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 3 by A22, A17, A18, A11, Th6

.= (((0,1) --> (1,3)) ") . 3 by A55, A61, FUNCT_4:16

.= 1 by A52, FUNCT_4:63 ;

let a, b be Element of (Necklace 4); :: thesis: ( not a = F . x or not b = F . y or a <= b )

assume that

A63: a = F . x and

A64: b = F . y ; :: thesis: a <= b

per cases
( ( x = 0 & y = 0 ) or ( x = 0 & y = 1 ) or ( x = 0 & y = 2 ) or ( x = 0 & y = 3 ) or ( x = 1 & y = 0 ) or ( x = 1 & y = 1 ) or ( x = 1 & y = 2 ) or ( x = 1 & y = 3 ) or ( x = 2 & y = 0 ) or ( x = 2 & y = 1 ) or ( x = 2 & y = 2 ) or ( x = 2 & y = 3 ) or ( x = 3 & y = 0 ) or ( x = 3 & y = 1 ) or ( x = 3 & y = 2 ) or ( x = 3 & y = 3 ) )
by A41, CARD_1:52, ENUMSET1:def 2;

end;

suppose A65:
( x = 0 & y = 2 )
; :: thesis: a <= b

then
b = 2 + 1
by A64, A60;

then [a,b] in the InternalRel of (Necklace 4) by A63, A51, A65, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

end;then [a,b] in the InternalRel of (Necklace 4) by A63, A51, A65, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

suppose A66:
( x = 0 & y = 3 )
; :: thesis: a <= b

then
a = 1 + 1
by A63, A51;

then [a,b] in the InternalRel of (Necklace 4) by A64, A62, A66, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

end;then [a,b] in the InternalRel of (Necklace 4) by A64, A62, A66, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

suppose A67:
( x = 1 & y = 3 )
; :: thesis: a <= b

then
b = 0 + 1
by A64, A62;

then [a,b] in the InternalRel of (Necklace 4) by A63, A58, A67, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

end;then [a,b] in the InternalRel of (Necklace 4) by A63, A58, A67, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

suppose A68:
( x = 2 & y = 0 )
; :: thesis: a <= b

then
a = 2 + 1
by A63, A60;

then [a,b] in the InternalRel of (Necklace 4) by A64, A51, A68, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

end;then [a,b] in the InternalRel of (Necklace 4) by A64, A51, A68, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

suppose A69:
( x = 3 & y = 0 )
; :: thesis: a <= b

then
b = 1 + 1
by A64, A51;

then [a,b] in the InternalRel of (Necklace 4) by A63, A62, A69, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

end;then [a,b] in the InternalRel of (Necklace 4) by A63, A62, A69, Th24;

hence a <= b by ORDERS_2:def 5; :: thesis: verum

case
( Necklace 4 is empty or ComplRelStr (Necklace 4) is empty )
; :: thesis: ( Necklace 4 is empty & ComplRelStr (Necklace 4) is empty )

end;

end;