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))
proof
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;
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
.= {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 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 b1 being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st
( b1 = f " & b1 is monotone ) )
set A = the InternalRel of (ComplRelStr (Necklace 4));
A8: rng (0 .--> 1) misses rng (1 .--> 3)
proof
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;
A11: rng ((0,1) --> (1,3)) misses rng ((2,3) --> (0,2))
proof
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;
set B = {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]};
A14: rng (2 .--> 0) misses rng (3 .--> 2)
proof
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;
(2,3) --> (0,2) = (2 .--> 0) +* (3 .--> 2) by FUNCT_4:def 4;
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
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 A21: rng f = (rng ((0,1) --> (1,3))) \/ (rng ((2,3) --> (0,2))) by FRECHET:35, PARTFUN1:56
.= {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 one-to-one by A17, A11, FUNCT_4:92; :: thesis: ( f is monotone & ex b1 being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st
( b1 = f " & b1 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))
proof
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)
proof
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 A27: x9 in the InternalRel of (Necklace 4) ` by SUBSET_1:29;
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;
thus f is monotone :: thesis: ex b1 being Element of bool [: the carrier of (ComplRelStr (Necklace 4)), the carrier of (Necklace 4):] st
( b1 = f " & b1 is monotone )
proof
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 b1, b2 being Element of the carrier of (ComplRelStr (Necklace 4)) holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 ) )
assume x <= y ; :: thesis: for b1, b2 being Element of the carrier of (ComplRelStr (Necklace 4)) holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )
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;
suppose ( x = 0 & y = 0 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
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;
suppose ( x = 0 & y = 2 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
suppose ( x = 0 & y = 3 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
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;
suppose ( x = 1 & y = 1 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
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;
suppose ( x = 1 & y = 3 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
suppose ( x = 2 & y = 0 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
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;
suppose ( x = 2 & y = 2 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
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;
suppose ( x = 3 & y = 0 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
suppose ( x = 3 & y = 1 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
suppose ( x = 3 & y = 2 ) ; :: 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;
suppose ( x = 3 & y = 3 ) ; :: thesis: a <= b
hence a <= b by A35; :: thesis: verum
end;
end;
end;
take F ; :: thesis: ( F = f " & F is monotone )
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 b1, b2 being Element of the carrier of (Necklace 4) holds
( not b1 = F . x or not b2 = F . y or b1 <= b2 ) )
assume x <= y ; :: thesis: for b1, b2 being Element of the carrier of (Necklace 4) holds
( not b1 = F . x or not b2 = F . y or b1 <= b2 )
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
hereby :: thesis: i <> j
assume A45: ( i + 1 = j or j + 1 = i ) ; :: thesis: contradiction
per cases ( i + 1 = j or j + 1 = i ) by A45;
end;
end;
thus i <> j by A38, A42, Def8; :: thesis: verum
end;
A48: ((2,3) --> (0,2)) " = (0,2) --> (2,3) by Th9;
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
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;
A58: F . 1 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 1 by A22, A17, A18, A11, Th6
.= (((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;
suppose ( x = 0 & y = 0 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 0 & y = 1 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 1 & y = 0 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 1 & y = 1 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 1 & y = 2 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 2 & y = 1 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 2 & y = 2 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 2 & y = 3 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 3 & y = 2 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
suppose ( x = 3 & y = 3 ) ; :: thesis: a <= b
hence a <= b by A44; :: thesis: verum
end;
end;
end;
end;
case ( Necklace 4 is empty or ComplRelStr (Necklace 4) is empty ) ; :: thesis: ( Necklace 4 is empty & ComplRelStr (Necklace 4) is empty )
hence ( Necklace 4 is empty & ComplRelStr (Necklace 4) is empty ) ; :: thesis: verum
end;
end;