let x, X, y be set ; :: 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 Element of 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 Element of 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 Element of 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 Element of 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 Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) implies [x,y] in EqR1 "\/" EqR2 )

proof

assume A2: [x,y] in EqR1 "\/" EqR2 ; :: thesis: ex f being FinSequence st
( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) )
defpred S₁[ set , set ] means ex f being FinSequence st
( 1 <= len f & $1 = f . 1 & $2 = f . (len f) & ( for i being Element of 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
A3: for x, y being set holds
( [x,y] in Y iff ( x in X & y in X & S₁[x,y] ) ) from RELSET_1:sch 1();
A4: Y is_reflexive_in X

proof

let x be set ; :: according to RELAT_2:def 1 :: thesis: ( not x in X or [x,x] in Y )
assume A5: x in X ; :: thesis: [x,x] in Y
set g = <*x*>;
A6: ( len <*x*> = 1 & <*x*> . 1 = x ) by FINSEQ_1:57;
for i being Element of NAT st 1 <= i & i < len <*x*> holds
[(<*x*> . i),(<*x*> . (i + 1))] in EqR1 \/ EqR2 by FINSEQ_1:57;
hence [x,x] in Y by A3, A5, A6; :: thesis: verum

end;

A7: Y is_symmetric_in X

proof

let x be set ; :: according to RELAT_2:def 3 :: thesis: for b₁ being set holds
( not x in X or not b₁ in X or not [x,b₁] in Y or [b₁,x] in Y )
let y be set ; :: thesis: ( not x in X or not y in X or not [x,y] in Y or [y,x] in Y )
assume A8: ( x in X & y in X & [x,y] in Y ) ; :: thesis: [y,x] in Y
then consider f being FinSequence such that
A9: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A3;
defpred S₂[ Nat, set ] means $2 = f . ((1 + (len f)) - $1);
A11: for k being Nat st k in Seg (len f) holds
ex z being set st S₂[k,z] ;
consider g being FinSequence such that
A12: ( dom g = Seg (len f) & ( for k being Nat st k in Seg (len f) holds
S₂[k,g . k] ) ) from FINSEQ_1:sch 1(A11);
A13: len f = len g by A12, FINSEQ_1:def 3;
A14: 1 <= len g by A9, A12, FINSEQ_1:def 3;

A15: now

1 in Seg (len f) by A9, FINSEQ_1:3;
then g . 1 = f . (((len f) + 1) - 1) by A12
.= f . (len f) ;
hence y = g . 1 by A9; :: thesis: verum

end;

A16: now

len f in Seg (len f) by A9, FINSEQ_1:3;
then g . (len f) = f . ((1 + (len f)) - (len f)) by A12
.= f . (1 + 0 ) ;
hence x = g . (len g) by A9, A12, FINSEQ_1:def 3; :: thesis: verum

end;

for j being Element of NAT st 1 <= j & j < len g holds
[(g . j),(g . (j + 1))] in EqR1 \/ EqR2

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 )
assume A17: ( 1 <= j & j < len g ) ; :: thesis: [(g . j),(g . (j + 1))] in EqR1 \/ EqR2
then j in Seg (len f) by A13, FINSEQ_1:3;
then A18: g . j = f . ((1 + (len f)) - j) by A12
.= f . (((len f) - j) + 1) ;
A19: 1 <= j + 1 by NAT_1:12;
j + 1 <= len f by A13, A17, NAT_1:13;
then j + 1 in Seg (len f) by A19, FINSEQ_1:3;
then A20: g . (j + 1) = f . (((len f) + 1) - (1 + j)) by A12
.= f . ((len f) - j) ;
reconsider k = (len f) - j as Element of NAT by A13, A17, NAT_1:21;
j - (len f) < (len f) - (len f) by A13, A17, XREAL_1:11;
then - ((len f) - j) < - 0 ;
then 0 < k ;
then A21: 0 + 1 <= k by NAT_1:13;
- j < - 0 by A17, XREAL_1:26;
then (len f) + (- j) < 0 + (len f) by XREAL_1:8;
then A22: [(f . k),(f . (k + 1))] in EqR1 \/ EqR2 by A9, A21;

now

per cases ( [(f . k),(f . (k + 1))] in EqR1 or [(f . k),(f . (k + 1))] in EqR2 ) by A22, 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 Th12;
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 Th12;
hence [(f . (k + 1)),(f . k)] in EqR1 \/ EqR2 by XBOOLE_0:def 3; :: thesis: verum

end;

end;

end;

hence [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 by A18, A20; :: thesis: verum

end;

hence [y,x] in Y by A3, A8, A14, A15, A16; :: thesis: verum

end;

A23: Y is_transitive_in X

proof

let x be set ; :: according to RELAT_2:def 8 :: thesis: for b₁, b₂ being set holds
( not x in X or not b₁ in X or not b₂ in X or not [x,b₁] in Y or not [b₁,b₂] in Y or [x,b₂] in Y )
let y, z be set ; :: 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 A24: ( x in X & y in X & z in X & [x,y] in Y & [y,z] in Y ) ; :: thesis: [x,z] in Y
then consider f being FinSequence such that
A25: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A3;
consider g being FinSequence such that
A26: ( 1 <= len g & y = g . 1 & z = g . (len g) & ( for i being Element of NAT st 1 <= i & i < len g holds
[(g . i),(g . (i + 1))] in EqR1 \/ EqR2 ) ) by A3, A24;
set h = f ^ g;
A27: len (f ^ g) = (len f) + (len g) by FINSEQ_1:35;
then A28: 1 <= len (f ^ g) by A25, NAT_1:12;
1 in Seg (len f) by A25, FINSEQ_1:3;
then 1 in dom f by FINSEQ_1:def 3;
then A29: x = (f ^ g) . 1 by A25, FINSEQ_1:def 7;
A30: (len f) + 1 <= (len f) + (len g) by A26, XREAL_1:9;
then A31: (f ^ g) . (len (f ^ g)) = g . (((len g) + (len f)) - (len f)) by A27, FINSEQ_1:36
.= g . (len g) ;
for i being Element of NAT st 1 <= i & i < len (f ^ g) holds
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len (f ^ g) implies [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 )
assume A32: ( 1 <= i & i < len (f ^ g) ) ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
then A33: ( ( 1 <= i & i < len f ) or i = len f or len f < i ) by XXREAL_0:1;

now

per cases ( ( 1 <= i & i < len f ) or i = len f or ( (len f) + 1 <= i & i < len (f ^ g) ) ) by A32, A33, NAT_1:13;

suppose A34: ( 1 <= i & i < len f ) ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2

then i in Seg (len f) by FINSEQ_1:3;
then i in dom f by FINSEQ_1:def 3;
then A35: (f ^ g) . i = f . i by FINSEQ_1:def 7;
( 1 <= i + 1 & i + 1 <= len f ) by A34, NAT_1:13;
then i + 1 in Seg (len f) by FINSEQ_1:3;
then i + 1 in dom f by FINSEQ_1:def 3;
then (f ^ g) . (i + 1) = f . (i + 1) by FINSEQ_1:def 7;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A25, A34, A35; :: thesis: verum

end;

suppose A36: i = len f ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2

len f in Seg (len f) by A25, FINSEQ_1:3;
then len f in dom f by FINSEQ_1:def 3;
then A37: (f ^ g) . i = y by A25, A36, FINSEQ_1:def 7;
A38: (f ^ g) . (i + 1) = g . ((1 + (len f)) - (len f)) by A30, A36, FINSEQ_1:36
.= y by A26 ;
[y,y] in EqR1 by A24, Th11;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A37, A38, XBOOLE_0:def 3; :: thesis: verum

end;

suppose A39: ( (len f) + 1 <= i & i < len (f ^ g) ) ; :: thesis: [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2

then ( (len f) + 1 <= i + 1 & i + 1 <= (len f) + (len g) ) by A27, NAT_1:13;
then A40: (f ^ g) . (i + 1) = g . ((1 + i) - (len f)) by FINSEQ_1:36
.= g . ((i - (len f)) + 1) ;
( 1 <= len f & len f < i ) by A25, A39, NAT_1:13;
then reconsider k = i - (len f) as Element of NAT by NAT_1:21;
( (1 + (len f)) - (len f) <= i - (len f) & i < (len f) + (len g) ) by A39, FINSEQ_1:35, XREAL_1:11;
then ( 1 <= i - (len f) & i - (len f) < len g ) by XREAL_1:21;
then [(g . k),(g . (k + 1))] in EqR1 \/ EqR2 by A26;
hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 by A27, A39, A40, FINSEQ_1:36; :: thesis: verum

end;

end;

end;

hence [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2 ; :: thesis: verum

end;

hence [x,z] in Y by A3, A24, A26, A28, A29, A31; :: thesis: verum

end;

( field Y = X & dom Y = X ) by A4, ORDERS_1:98;
then reconsider R1 = Y as Equivalence_Relation of X by A7, A23, PARTFUN1:def 4, RELAT_2:def 11, RELAT_2:def 16;
for x, y being set st [x,y] in EqR1 \/ EqR2 holds
[x,y] in R1

proof

let x, y be set ; :: thesis: ( [x,y] in EqR1 \/ EqR2 implies [x,y] in R1 )
assume A41: [x,y] in EqR1 \/ EqR2 ; :: thesis: [x,y] in R1
then A42: ( x in X & y in X ) by Lm1;
set g = <*x,y*>;
A43: len <*x,y*> = 2 by FINSEQ_1:61;
A44: len <*x,y*> = 1 + 1 by FINSEQ_1:61;
A45: ( <*x,y*> . 1 = x & <*x,y*> . 2 = y ) by FINSEQ_1:61;
A46: ( <*x,y*> . 1 = x & <*x,y*> . (len <*x,y*>) = y ) by A43, FINSEQ_1:61;
for i being Element of NAT st 1 <= i & i < len <*x,y*> holds
[(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2

proof

let i be Element of NAT ; :: thesis: ( 1 <= i & i < len <*x,y*> implies [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 )
assume ( 1 <= i & i < len <*x,y*> ) ; :: thesis: [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2
then ( 1 <= i & i <= 1 ) by A44, NAT_1:13;
then 1 = i by XXREAL_0:1;
hence [(<*x,y*> . i),(<*x,y*> . (i + 1))] in EqR1 \/ EqR2 by A41, A45; :: thesis: verum

end;

hence [x,y] in R1 by A3, A42, A44, A46; :: thesis: verum

end;

then EqR1 \/ EqR2 c= R1 by RELAT_1:def 3;
then EqR1 "\/" EqR2 c= R1 by Def3;
then consider f being FinSequence such that
A47: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A2, A3;
take f ; :: thesis: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of 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 Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) by A47; :: thesis: verum

end;

given f being FinSequence such that A48: ( 1 <= len f & x = f . 1 & y = f . (len f) & ( for i being Element of NAT st 1 <= i & i < len f holds
[(f . i),(f . (i + 1))] in EqR1 \/ EqR2 ) ) ; :: thesis: [x,y] in EqR1 "\/" EqR2
defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in EqR1 "\/" EqR2 );
for i being Element of NAT holds S₁[i]

proof

A49: S₁[ 0 ] ;

A50: now

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A51: S₁[i] ; :: thesis: S₁[i + 1]
thus S₁[i + 1] :: thesis: verum

proof

assume A52: ( 1 <= i + 1 & i + 1 <= len f ) ; :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2
then A53: i < len f by NAT_1:13;
A54: ( 1 <= i or 1 = i + 1 ) by A52, NAT_1:8;
A55: EqR1 \/ EqR2 c= EqR1 "\/" EqR2 by Def3;

now

per cases ( 1 <= i or 0 = i ) by A54;

suppose A56: 1 <= i ; :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2

then [(f . i),(f . (i + 1))] in EqR1 \/ EqR2 by A48, A53;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A51, A52, A55, A56, Th13, NAT_1:13; :: thesis: verum

end;

suppose A57: 0 = i ; :: thesis: [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2

[(f . 1),(f . 1)] in EqR1 by A1, A48, Th11;
then [(f . 1),(f . 1)] in EqR1 \/ EqR2 by XBOOLE_0:def 3;
hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 by A55, A57; :: thesis: verum

end;

end;

end;

hence [(f . 1),(f . (i + 1))] in EqR1 "\/" EqR2 ; :: thesis: verum

end;

end;

thus for i being Element of NAT holds S₁[i] from NAT_1:sch 1(A49, A50); :: thesis: verum

end;

hence [x,y] in EqR1 "\/" EqR2 by A48; :: thesis: verum