let Y be non empty set ; :: thesis: for R1, R2 being Equivalence_Relation of Y
for f being FinSequence of Y
for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
let R1, R2 be Equivalence_Relation of Y; :: thesis: for f being FinSequence of Y
for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
let f be FinSequence of Y; :: thesis: for x, y being set st x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) holds
[x,y] in R1 "\/" R2
let x, y be set ; :: thesis: ( x in Y & f . 1 = x & f . (len f) = y & 1 <= len f & ( for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ) implies [x,y] in R1 "\/" R2 )
assume that
A1: x in Y and
A2: f . 1 = x and
A3: ( f . (len f) = y & 1 <= len f ) and
A4: for i being Element of NAT st 1 <= i & i < len f holds
ex u being set st
( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) ; :: thesis: [x,y] in R1 "\/" R2
for i being Element of NAT st 1 <= i & i <= len f holds
[(f . 1),(f . i)] in R1 "\/" R2

proof

defpred S₁[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in R1 "\/" R2 );
A6: S₁[ 0 ] ;
A7: for i being Element of NAT st S₁[i] holds
S₁[i + 1]

proof

let i be Element of NAT ; :: thesis: ( S₁[i] implies S₁[i + 1] )
assume A8: S₁[i] ; :: thesis: S₁[i + 1]
assume that
A9: 1 <= i + 1 and
A10: i + 1 <= len f ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
A11: i < len f by A10, NAT_1:13;
A12: ( 1 <= i or 1 = i + 1 ) by A9, NAT_1:8;
A13: R1 \/ R2 c= R1 "\/" R2 by EQREL_1:def 3;

now

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

suppose A15: 1 <= i ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2

then consider u being set such that
A16: u in Y and
A17: ( [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) by A4, A11;
reconsider u = u as Element of Y by A16;
A18: dom f = Seg (len f) by FINSEQ_1:def 3;
then i in dom f by A11, A15, FINSEQ_1:3;
then reconsider f1 = f . i as Element of Y by FINSEQ_2:13;
i + 1 in dom f by A9, A10, A18, FINSEQ_1:3;
then reconsider f2 = f . (i + 1) as Element of Y by FINSEQ_2:13;
reconsider p = <*f1,u,f2*> as FinSequence of Y ;
A21: len p = 3 by FINSEQ_1:62;
A22: ( p . 1 = f . i & p . 3 = f . (i + 1) ) by FINSEQ_1:62;
for j being Element of NAT st 1 <= j & j < len p holds
[(p . j),(p . (j + 1))] in R1 \/ R2

proof

let j be Element of NAT ; :: thesis: ( 1 <= j & j < len p implies [(p . j),(p . (j + 1))] in R1 \/ R2 )
assume that
A24: 1 <= j and
A25: j < len p ; :: thesis: [(p . j),(p . (j + 1))] in R1 \/ R2
j < 2 + 1 by A25, FINSEQ_1:62;
then j <= 2 by NAT_1:13;
then ( j = 0 or j = 1 or j = 2 ) by NAT_1:27;
hence [(p . j),(p . (j + 1))] in R1 \/ R2 by A17, A22, A24, FINSEQ_1:62; :: thesis: verum

end;

then [(f . i),(f . (i + 1))] in R1 "\/" R2 by A21, A22, EQREL_1:36;
hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A8, A10, A15, EQREL_1:13, NAT_1:13; :: thesis: verum

end;

suppose A30: 0 = i ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2

[(f . 1),(f . 1)] in R1 by A1, A2, EQREL_1:11;
then [(f . 1),(f . 1)] in R1 \/ R2 by XBOOLE_0:def 3;
hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A13, A30; :: thesis: verum

end;

end;

end;

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

end;

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

end;

hence [x,y] in R1 "\/" R2 by A2, A3; :: thesis: verum