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 )

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 S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in EqR1 "\/" EqR2 );

_{1}[ 0 ]
;

for i being Nat holds S_{1}[i]
from NAT_1:sch 2(A76, A67);

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

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

given f being FinSequence such that A63:
1 <= len f
and
defpred S_{1}[ 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 & S_{1}[x,y] ) )
from RELSET_1:sch 1();

A3: Y is_transitive_in X

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

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;( 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 & S

A3: Y is_transitive_in X

proof

A33:
Y is_symmetric_in X
let x be object ; :: according to RELAT_2:def 8 :: thesis: for b_{1}, b_{2} being object holds

( not x in X or not b_{1} in X or not b_{2} in X or not [x,b_{1}] in Y or not [b_{1},b_{2}] in Y or [x,b_{2}] 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

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;( not x in X or not b

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

1 in Seg (len f)
by A13, FINSEQ_1:1;
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;

end;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 \/ EqR2end;

hence
[((f ^ g) . i),((f ^ g) . (i + 1))] in EqR1 \/ EqR2
; :: thesis: verumper 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;

end;

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;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

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;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

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;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

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

proof

Y is_reflexive_in X
let x be object ; :: according to RELAT_2:def 3 :: thesis: for b_{1} being object holds

( not x in X or not b_{1} in X or not [x,b_{1}] in Y or [b_{1},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 S_{2}[ 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 S_{2}[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

S_{2}[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

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;( not x in X or not b

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 S

A40: for k being Nat st k in Seg (len f) holds

ex z being object st S

consider g being FinSequence such that

A41: ( dom g = Seg (len f) & ( for k being Nat st k in Seg (len f) holds

S

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

len f in Seg (len f)
by A36, FINSEQ_1:1;
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;

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;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 \/ EqR2end;

( 1 <= j + 1 & j + 1 <= len f )
by A42, A45, NAT_1:12, NAT_1:13;per cases
( [(f . k),(f . (k + 1))] in EqR1 or [(f . k),(f . (k + 1))] in EqR2 )
by A47, XBOOLE_0:def 3;

end;

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

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

proof

then
( field Y = X & dom Y = X )
by ORDERS_1:13;
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;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

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

then
EqR1 \/ EqR2 c= R1
;
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

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;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

len <*x,y*> = 2
by FINSEQ_1:44;
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;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

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

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

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 S

A67: now :: thesis: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]

A76:
SS

let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A68: S_{1}[i]
; :: thesis: S_{1}[i + 1]

thus S_{1}[i + 1]
:: thesis: verum

end;assume A68: S

thus S

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;

end;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

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

for i being Nat holds S

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