let X be set ; 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 ; 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; ( 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
; ( [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 ) ) )
( 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 ;
RELAT_2:def 8 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 ;
( 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
;
[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;
( 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)
;
[((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 [((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2per 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 A26:
i = len f
;
[((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;
verum end; suppose A29:
(
(len f) + 1
<= i &
i < len (f ^ g) )
;
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2then
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;
verum end; end; end;
hence
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
;
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;
verum
end;
A33:
Y is_symmetric_in X
proof
let x be
object ;
RELAT_2:def 3 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 ;
( 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
;
[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;
( 1 <= j & j < len g implies [(g . j),(g . (j + 1))] in EqR1 \/ EqR2 )
assume that A44:
1
<= j
and A45:
j < len g
;
[(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;
( 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;
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;
verum
end;
Y is_reflexive_in X
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 ;
( [x,y] in EqR1 \/ EqR2 implies [x,y] in R1 )
assume A54:
[x,y] in EqR1 \/ EqR2
;
[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;
( 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*>
;
[(<*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;
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;
verum
end;
then
EqR1 \/ EqR2 c= R1
;
then A61:
EqR1 "\/" EqR2 c= R1
by Def2;
assume
[x,y] in EqR1 "\/" EqR2
;
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
;
( 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;
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
; [x,y] in EqR1 "\/" EqR2
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in EqR1 "\/" EqR2 );
A67:
now for i being Nat st S1[i] holds
S1[i + 1]let i be
Nat;
( S1[i] implies S1[i + 1] )assume A68:
S1[
i]
;
S1[i + 1]thus
S1[
i + 1]
verum 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; verum