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 ();
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 ()
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 () )
assume A4: x in rng (((0,1) --> (1,3)) +* ((2,3) --> (0,2))) ; :: thesis: x in the carrier of ()
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
.= {0,1,2,3} by ENUMSET1:69 ;
then x in 4 by ;
then x in the carrier of () by Th19;
hence x in the carrier of () 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 () by ;
then reconsider f = ((0,1) --> (1,3)) +* ((2,3) --> (0,2)) as Function of (),() by ;
take f ; :: according to WAYBEL_1:def 8 :: thesis: f is isomorphic
per cases ( ( not Necklace 4 is empty & not ComplRelStr () is empty ) or Necklace 4 is empty or ComplRelStr () is empty ) ;
:: according to WAYBEL_0:def 38
case that not Necklace 4 is empty and
not ComplRelStr () is empty ; :: thesis: ( f is one-to-one & f is monotone & ex b1 being Element of bool [: the carrier of (), the carrier of ():] st
( b1 = f " & b1 is monotone ) )

set A = the InternalRel of ();
A8: rng () misses rng (1 .--> 3)
proof
assume rng () meets rng (1 .--> 3) ; :: thesis: contradiction
then consider x being object such that
A9: x in rng () and
A10: x in rng (1 .--> 3) by XBOOLE_0:3;
rng () = {1} by FUNCOP_1:8;
then ( rng (1 .--> 3) = {3} & x = 1 ) by ;
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 ;
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 () misses rng (3 .--> 2)
proof
assume rng () meets rng (3 .--> 2) ; :: thesis: contradiction
then consider x being object such that
A15: x in rng () and
A16: x in rng (3 .--> 2) by XBOOLE_0:3;
rng () = by FUNCOP_1:8;
then ( rng (3 .--> 2) = {2} & x = 0 ) by ;
hence contradiction by A16, TARSKI:def 1; :: thesis: verum
end;
(2,3) --> (0,2) = () +* (3 .--> 2) by FUNCT_4:def 4;
then A17: (2,3) --> (0,2) is one-to-one by ;
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 ;
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
.= {1,3,0,2} by
.= {0,1,2,3} by ENUMSET1:69
.= the carrier of () by
.= the carrier of () by Def8 ;
(0,1) --> (1,3) = () +* (1 .--> 3) by FUNCT_4:def 4;
then A22: (0,1) --> (1,3) is one-to-one by ;
hence f is V7() by ; :: thesis: ( f is monotone & ex b1 being Element of bool [: the carrier of (), the carrier of ():] st
( b1 = f " & b1 is monotone ) )

then reconsider F = f " as Function of (),() by ;
A23: {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} c= the InternalRel of ()
proof
set C = the carrier of ();
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 () )
assume x in {[1,3],[3,1],[0,2],[2,0],[0,3],[3,0]} ; :: thesis: x in the InternalRel of ()
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 () & 3 in the carrier of () ) by ;
( 0 in the carrier of () & 1 in the carrier of () ) by ;
then reconsider x9 = x as Element of [: the carrier of (), the carrier of ():] by ;
not x9 in the InternalRel of ()
proof
assume x9 in the InternalRel of () ; :: 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 ;
hence contradiction ; :: thesis: verum
end;
then A27: x9 in the InternalRel of () ` by SUBSET_1:29;
not x in id the carrier of () by ;
then x in ( the InternalRel of () `) \ (id the carrier of ()) by ;
hence x in the InternalRel of () by Def8; :: thesis: verum
end;
thus f is monotone :: thesis: ex b1 being Element of bool [: the carrier of (), the carrier of ():] 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 ;
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
.= 1 by FUNCT_4:63 ;
1 in dom ((0,1) --> (1,3)) by ;
then A33: f . 1 = ((0,1) --> (1,3)) . 1 by
.= 3 by FUNCT_4:63 ;
let x, y be Element of (); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of () 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 () holds
( not b1 = f . x or not b2 = f . y or b1 <= b2 )

then A34: [x,y] in the InternalRel of () by ORDERS_2:def 5;
the carrier of () = 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 ;
let a, b be Element of (); :: 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 ;
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 ;
hence a <= b by ; :: 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 ;
hence a <= b by ; :: 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 ;
hence a <= b by ; :: 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 ;
hence a <= b by ; :: 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 ;
hence a <= b by ; :: 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 ;
hence a <= b by ; :: 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 (); :: according to ORDERS_3:def 5 :: thesis: ( not x <= y or for b1, b2 being Element of the carrier of () 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 () holds
( not b1 = F . x or not b2 = F . y or b1 <= b2 )

then [x,y] in the InternalRel of () by ORDERS_2:def 5;
then A37: [x,y] in ( the InternalRel of () `) \ (id the carrier of ()) by Def8;
then not [x,y] in id the carrier of () by XBOOLE_0:def 5;
then A38: ( not x in the carrier of () or x <> y ) by RELAT_1:def 10;
( [x,y] in the InternalRel of () ` implies not [x,y] in the InternalRel of () ) 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 ;
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 () = the carrier of () 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 () ;
A43: not [x,y] in { [k,(k + 1)] where k is Element of NAT : k + 1 < 4 } by ;
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;
suppose A46: i + 1 = j ; :: thesis: contradiction
end;
suppose A47: j + 1 = i ; :: thesis: contradiction
end;
end;
end;
thus i <> j by ; :: 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
.= 2 by ;
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 ;
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
.= 0 by ;
A59: 2 in dom (((2,3) --> (0,2)) ") by ;
A60: F . 2 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 2 by A22, A17, A18, A11, Th6
.= (((2,3) --> (0,2)) ") . 2 by
.= 3 by ;
A61: 3 in dom (((0,1) --> (1,3)) ") by ;
A62: F . 3 = ((((0,1) --> (1,3)) ") +* (((2,3) --> (0,2)) ")) . 3 by A22, A17, A18, A11, Th6
.= (((0,1) --> (1,3)) ") . 3 by
.= 1 by ;
let a, b be Element of (); :: 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 ;
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 A65: ( x = 0 & y = 2 ) ; :: thesis: a <= b
then b = 2 + 1 by ;
then [a,b] in the InternalRel of () by ;
hence a <= b by ORDERS_2:def 5; :: thesis: verum
end;
suppose A66: ( x = 0 & y = 3 ) ; :: thesis: a <= b
then a = 1 + 1 by ;
then [a,b] in the InternalRel of () by ;
hence a <= b by ORDERS_2:def 5; :: 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 A67: ( x = 1 & y = 3 ) ; :: thesis: a <= b
then b = 0 + 1 by ;
then [a,b] in the InternalRel of () by ;
hence a <= b by ORDERS_2:def 5; :: thesis: verum
end;
suppose A68: ( x = 2 & y = 0 ) ; :: thesis: a <= b
then a = 2 + 1 by ;
then [a,b] in the InternalRel of () by ;
hence a <= b by ORDERS_2:def 5; :: 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 A69: ( x = 3 & y = 0 ) ; :: thesis: a <= b
then b = 1 + 1 by ;
then [a,b] in the InternalRel of () by ;
hence a <= b by ORDERS_2:def 5; :: thesis: verum
end;
suppose A70: ( x = 3 & y = 1 ) ; :: thesis: a <= b
then a = 0 + 1 by ;
then [a,b] in the InternalRel of () by ;
hence a <= b by ORDERS_2:def 5; :: 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 () is empty ) ; :: thesis: ( Necklace 4 is empty & ComplRelStr () is empty )
hence ( Necklace 4 is empty & ComplRelStr () is empty ) ; :: thesis: verum
end;
end;