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 & y 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 & y 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 & y 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 & y 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 A1: ( x in Y & y 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 ) ) ) ; :: 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 S1[ Element of NAT ] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in R1 "\/" R2 );
A2: S1[ 0 ] ;
A3: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume A4: S1[i] ; :: thesis: S1[i + 1]
assume A5: ( 1 <= i + 1 & i + 1 <= len f ) ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
then A6: i < len f by NAT_1:13;
A7: ( 1 <= i or 1 = i + 1 ) by A5, NAT_1:8;
A8: R1 \/ R2 c= R1 "\/" R2 by EQREL_1:def 3;
now
per cases ( 1 <= i or 0 = i ) by A7;
suppose A9: 1 <= i ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
then consider u being set such that
A10: ( u in Y & [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) by A1, A6;
reconsider u = u as Element of Y by A10;
A11: dom f = Seg (len f) by FINSEQ_1:def 3;
then i in dom f by A6, A9, FINSEQ_1:3;
then reconsider f1 = f . i as Element of Y by FINSEQ_2:13;
i + 1 in dom f by A5, A11, 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 ;
A12: ( len p = 3 & p . 1 = f . i & p . 2 = u & 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 ( 1 <= j & j < len p ) ; :: thesis: [(p . j),(p . (j + 1))] in R1 \/ R2
then ( 1 <= j & j < 2 + 1 ) by FINSEQ_1:62;
then ( 1 <= j & j <= 2 ) by NAT_1:13;
then ( 1 <= j & ( j = 0 or j = 1 or j = 2 ) ) by NAT_1:27;
hence [(p . j),(p . (j + 1))] in R1 \/ R2 by A10, A12; :: thesis: verum
end;
then [(f . i),(f . (i + 1))] in R1 "\/" R2 by A12, EQREL_1:36;
hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A4, A5, A9, EQREL_1:13, NAT_1:13; :: thesis: verum
end;
suppose A13: 0 = i ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
[(f . 1),(f . 1)] in R1 by A1, 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 A8, A13; :: 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 S1[i] from NAT_1:sch 1(A2, A3); :: thesis: verum
end;
hence [x,y] in R1 "\/" R2 by A1; :: thesis: verum