let X be set ; :: thesis: for x, y being object
for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
let x, y be object ; :: thesis: for EqR1, EqR2 being Equivalence_Relation of X st x in X holds
( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
let EqR1, EqR2 be Equivalence_Relation of X; :: thesis: ( x in X implies ( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ) )
assume A1: x in X ; :: thesis: ( [x,y] in EqR1 "\/" EqR2 iff ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) )
thus ( [x,y] in EqR1 "\/" EqR2 implies ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ) :: thesis: ( ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) implies [x,y] in EqR1 "\/" EqR2 )
proof
defpred S1[ object , object ] means ex f being FinSequence st
( 1 <= len f & $1 = f . 1 & $2 = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) );
consider Y being Relation of X,X such that
A2: for x, y being object holds
( [x,y] in Y iff ( x in X & y in X & S1[x,y] ) ) from RELSET_1:sch 1();
 A3: Y is_transitive_in X
proof
let x be object ; :: according to RELAT_2:def 8 :: thesis: for b1, b2 being object holds
( not x in X or not b1 in X or not b2 in X or not [x,b1] in Y or not [b1,b2] in Y or [x,b2] in Y )
let y, z be object ; :: thesis: ( not x in X or not y in X or not z in X or not [x,y] in Y or not [y,z] in Y or [x,z] in Y )
assume that
A4: x in X and
A5: y in X and
A6: z in X and
A7: [x,y] in Y and
A8: [y,z] in Y ; :: thesis: [x,z] in Y
consider g being FinSequence such that
A9: 1 <= len g and
A10: y = g . 1 and
A11: z = g . (len g) and
A12: for i being Nat st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in EqR1 \/ EqR2 by A2, A8;
consider f being FinSequence such that
A13: 1 <= len f and
A14: x = f . 1 and
A15: y = f . (len f) and
A16: for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A2, A7;
set h = f ^ g;
A17: len (f ^ g) = (len f) + (len g) by FINSEQ_1:22;
A18: (len f) + 1 <= (len f) + (len g) by A9, XREAL_1:7;
then A19: (f ^ g) . (len (f ^ g)) = g . (((len g) + (len f)) - (len f)) by A17, FINSEQ_1:23
.= g . (len g) ;
A20: for i being Nat st 1 <= i & i < len (f ^ g) holds
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
proof
let i be Nat; :: thesis: ( 1 <= i & i < len (f ^ g) implies [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 )
assume that
A21: 1 <= i and
A22: i < len (f ^ g) ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
A23: ( ( 1 <= i & i < len f ) or i = len f or len f < i ) by A21, XXREAL_0:1;
now :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
per cases ( ( 1 <= i & i < len f ) or i = len f or ( (len f) + 1 <= i & i < len (f ^ g) ) ) by A22, A23, NAT_1:13;
suppose A24: ( 1 <= i & i < len f ) ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then ( 1 <= i + 1 & i + 1 <= len f ) by NAT_1:13;
then i + 1 in Seg (len f) by FINSEQ_1:1;
then i + 1 in dom f by FINSEQ_1:def 3;
then A25: (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def 7;
i in Seg (len f) by A24, FINSEQ_1:1;
then i in dom f by FINSEQ_1:def 3;
then (f ^ g) . i = f . i by FINSEQ_1:def 7;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A16, A24, A25; :: thesis: verum
end;
suppose A26: i = len f ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
len f in Seg (len f) by A13, FINSEQ_1:1;
then len f in dom f by FINSEQ_1:def 3;
then A27: (f ^ g) . i = y by A15, A26, FINSEQ_1:def 7;
A28: [y,y] in EqR1 by A5, Th5;
(f ^ g) . (i + 1) = g . ((1 + (len f)) - (len f)) by A18, A26, FINSEQ_1:23
.= y by A10 ;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A27, A28, XBOOLE_0:def 3; :: thesis: verum
end;
suppose A29: ( (len f) + 1 <= i & i < len (f ^ g) ) ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then len f < i by NAT_1:13;
then reconsider k = i - (len f) as Element of NAT by NAT_1:21;
i < (len f) + (len g) by A29, FINSEQ_1:22;
then A30: i - (len f) < len g by XREAL_1:19;
( (len f) + 1 <= i + 1 & i + 1 <= (len f) + (len g) ) by A17, A29, NAT_1:13;
then A31: (f ^ g) . (i + 1) = g . ((1 + i) - (len f)) by FINSEQ_1:23
.= g . ((i - (len f)) + 1) ;
(1 + (len f)) - (len f) <= i - (len f) by A29, XREAL_1:9;
then [(g . k),(g . (k + 1))] in EqR1 \/ EqR2 by A12, A30;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A17, A29, A31, FINSEQ_1:23; :: thesis: verum
end;
end;
end;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 ; :: thesis: verum
end;
1 in Seg (len f) by A13, FINSEQ_1:1;
then 1 in dom f by FINSEQ_1:def 3;
then A32: x = (f ^ g) . 1 by A14, FINSEQ_1:def 7;
1 <= len (f ^ g) by A13, A17, NAT_1:12;
hence [x,z] in Y by A2, A4, A6, A11, A32, A19, A20; :: thesis: verum
end;
A33: Y is_symmetric_in X
proof
let x be object ; :: according to RELAT_2:def 3 :: thesis: for b1 being object holds
( not x in X or not b1 in X or not [x,b1] in Y or [b1,x] in Y )
let y be object ; :: thesis: ( not x in X or not y in X or not [x,y] in Y or [y,x] in Y )
assume that
A34: ( x in X & y in X ) and
A35: [x,y] in Y ; :: thesis: [y,x] in Y
consider f being FinSequence such that
A36: 1 <= len f and
A37: x = f . 1 and
A38: y = f . (len f) and
A39: for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A2, A35;
defpred S2[ Nat, object ] means $2 = f . ((1 + (len f)) - $1);
A40: for k being Nat st k in Seg (len f) holds
ex z being object st S2[k,z] ;
consider g being FinSequence such that
A41: ( dom g = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S2[k,g . k] ) ) from FINSEQ_1:sch 1(A40);
 A42: len f = len g by A41, FINSEQ_1:def 3;
A43: for j being Nat st 1 <= j & j < len g holds
[(g . j),(g . (j + 1))] in EqR1 \/ EqR2
proof
let j be Nat; :: thesis: ( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 )
assume that
A44: 1 <= j and
A45: j < len g ; :: thesis: [(g . j),(g . (j + 1))] in EqR1 \/ EqR2
reconsider k = (len f) - j as Element of NAT by A42, A45, NAT_1:21;
j - (len f) < (len f) - (len f) by A42, A45, XREAL_1:9;
then - ((len f) - j) < - 0 ;
then 0 < k ;
then A46: 0 + 1 <= k by NAT_1:13;
- j < - 0 by A44, XREAL_1:24;
then (len f) + (- j) < 0 + (len f) by XREAL_1:6;
then A47: [(f . k),(f . (k + 1))] in EqR1 \/ EqR2 by A39, A46;
A48: now :: thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
per cases ( [(f . k),(f . (k + 1))] in EqR1 or [(f . k),(f . (k + 1))] in EqR2 ) by A47, XBOOLE_0:def 3;
suppose [(f . k),(f . (k + 1))] in EqR1 ; :: thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
then [(f . (k + 1)),(f . k)] in EqR1 by Th6;
hence [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def 3; :: thesis: verum
end;
suppose [(f . k),(f . (k + 1))] in EqR2 ; :: thesis: [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2
then [(f . (k + 1)),(f . k)] in EqR2 by Th6;
hence [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def 3; :: thesis: verum
end;
end;
end;
( 1 <= j + 1 & j + 1 <= len f ) by A42, A45, NAT_1:12, NAT_1:13;
then j + 1 in Seg (len f) by FINSEQ_1:1;
then A49: g . (j + 1) = f . (((len f) + 1) - (1 + j)) by A41
.= f . ((len f) - j) ;
j in Seg (len f) by A42, A44, A45, FINSEQ_1:1;
then g . j = f . ((1 + (len f)) - j) by A41
.= f . (((len f) - j) + 1) ;
hence [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 by A49, A48; :: thesis: verum
end;
len f in Seg (len f) by A36, FINSEQ_1:1;
then g . (len f) = f . ((1 + (len f)) - (len f)) by A41
.= f . (1 + 0) ;
then A50: x = g . (len g) by A37, A41, FINSEQ_1:def 3;
1 in Seg (len f) by A36, FINSEQ_1:1;
then A51: g . 1 = f . (((len f) + 1) - 1) by A41
.= f . (len f) ;
1 <= len g by A36, A41, FINSEQ_1:def 3;
hence [y,x] in Y by A2, A34, A38, A51, A50, A43; :: thesis: verum
end;
Y is_reflexive_in X
proof
let x be object ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in Y )
assume A52: x in X ; :: thesis: [x,x] in Y
set g = <*x*>;
A53: for i being Nat st 1 <= i & i < len <*x*> holds
[(<*x*> . i),(<*x*> . (i + 1))] in EqR1 \/ EqR2 by FINSEQ_1:40;
( len <*x*> = 1 & <*x*> . 1 = x ) by FINSEQ_1:40;
hence [x,x] in Y by A2, A52, A53; :: thesis: verum
end;
then ( field Y = X & dom Y = X ) by ORDERS_1:13;
then reconsider R1 = Y as Equivalence_Relation of X by A33, A3, PARTFUN1:def 2, RELAT_2:def 11, RELAT_2:def 16;
for x, y being object st [x,y] in EqR1 \/ EqR2 holds
[x,y] in R1
proof
let x, y be object ; :: thesis: ( [x,y] in EqR1 \/ EqR2 implies [x,y] in R1 )
assume A54: [x,y] in EqR1 \/ EqR2 ; :: thesis: [x,y] in R1
set g = <*x,y*>;
A55: len <*x,y*> = 1 + 1 by FINSEQ_1:44;
A56: <*x,y*> . 1 = x by FINSEQ_1:44;
A57: for i being Nat st 1 <= i & i < len <*x,y*> holds
[(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
proof
let i be Nat; :: thesis: ( 1 <= i & i < len <*x,y*> implies [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 )
assume that
A58: 1 <= i and
A59: i < len <*x,y*> ; :: thesis: [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
i <= 1 by A55, A59, NAT_1:13;
then 1 = i by A58, XXREAL_0:1;
hence [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 by A54, A56, FINSEQ_1:44; :: thesis: verum
end;
len <*x,y*> = 2 by FINSEQ_1:44;
then A60: ( <*x,y*> . 1 = x & <*x,y*> . (len <*x,y*>) = y ) by FINSEQ_1:44;
( x in X & y in X ) by A54, Lm1;
hence [x,y] in R1 by A2, A55, A60, A57; :: thesis: verum
end;
then EqR1 \/ EqR2 c= R1 ;
then A61: EqR1 "\/" EqR2 c= R1 by Def2;
assume [x,y] in EqR1 "\/" EqR2 ; :: thesis: ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
then consider f being FinSequence such that
A62: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A2, A61;
take f ; :: thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
thus ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A62; :: thesis: verum
end;
given f being FinSequence such that A63: 1 <= len f and
A64: x = f . 1 and
A65: y = f . (len f) and
A66: for i being Nat st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ; :: thesis: [x,y] in EqR1 "\/" EqR2
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in EqR1 "\/" EqR2 );
A67: now :: thesis: for i being Nat st S1[i] holds
S1[i + 1]
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A68: S1[i] ; :: thesis: S1[i + 1]
thus S1[i + 1] :: thesis: verum
proof
assume that
A69: 1 <= i + 1 and
A70: i + 1 <= len f ; :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
A71: ( 1 <= i or 1 = i + 1 ) by A69, NAT_1:8;
A72: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def2;
A73: i < len f by A70, NAT_1:13;
now :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
per cases ( 1 <= i or 0 = i ) by A71;
suppose A74: 1 <= i ; :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
then [(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A66, A73;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A68, A70, A72, A74, Th7, NAT_1:13; :: thesis: verum
end;
suppose A75: 0 = i ; :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
[(f . 1),(f . 1)] in EqR1 by A1, A64, Th5;
then [(f . 1),(f . 1)] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A72, A75; :: thesis: verum
end;
end;
end;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 ; :: thesis: verum
end;
end;
A76: S1[ 0 ] ;
for i being Nat holds S1[i] from NAT_1:sch 2(A76, A67);
 hence [x,y] in EqR1 "\/" EqR2 by A63, A64, A65; :: thesis: verum