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 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 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 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 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 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 Nat st 1 <= i & i <= len f holds
[(f . 1),(f . i)] in R1 "\/" R2
proof
defpred S1[ Nat] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in R1 "\/" R2 );
A5: S1[ 0 ] ;
A6: for i being Nat st S1[i] holds
S1[i + 1]
proof
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume A7: S1[i] ; :: thesis: S1[i + 1]
assume that
A8: 1 <= i + 1 and
A9: i + 1 <= len f ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
A10: i < len f by A9, NAT_1:13;
A11: ( 1 <= i or 1 = i + 1 ) by A8, NAT_1:8;
A12: R1 \/ R2 c= R1 "\/" R2 by EQREL_1:def 2;
now :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
per cases ( 1 <= i or 0 = i ) by A11;
suppose A13: 1 <= i ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
then consider u being set such that
A14: u in Y and
A15: ( [(f . i),u] in R1 \/ R2 & [u,(f . (i + 1))] in R1 \/ R2 ) by A4, A10;
reconsider u = u as Element of Y by A14;
A16: dom f = Seg (len f) by FINSEQ_1:def 3;
then i in dom f by A10, A13, FINSEQ_1:1;
then reconsider f1 = f . i as Element of Y by FINSEQ_2:11;
i + 1 in dom f by A8, A9, A16, FINSEQ_1:1;
then reconsider f2 = f . (i + 1) as Element of Y by FINSEQ_2:11;
reconsider p = <*f1,u,f2*> as FinSequence of Y ;
A17: len p = 3 by FINSEQ_1:45;
A18: ( p . 1 = f . i & p . 3 = f . (i + 1) ) by FINSEQ_1:45;
for j being Nat st 1 <= j & j < len p holds
[(p . j),(p . (j + 1))] in R1 \/ R2
proof
let j be Nat; :: thesis: ( 1 <= j & j < len p implies [(p . j),(p . (j + 1))] in R1 \/ R2 )
assume that
A19: 1 <= j and
A20: j < len p ; :: thesis: [(p . j),(p . (j + 1))] in R1 \/ R2
j < 2 + 1 by A20, FINSEQ_1:45;
then j <= 2 by NAT_1:13;
then not not j = 0 & ... & not j = 2 by NAT_1:60;
hence [(p . j),(p . (j + 1))] in R1 \/ R2 by A15, A18, A19, FINSEQ_1:45; :: thesis: verum
end;
then [(f . i),(f . (i + 1))] in R1 "\/" R2 by A17, A18, EQREL_1:28;
hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A7, A9, A13, EQREL_1:7, NAT_1:13; :: thesis: verum
end;
suppose A21: 0 = i ; :: thesis: [(f . 1),(f . (i + 1))] in R1 "\/" R2
[(f . 1),(f . 1)] in R1 by A1, A2, EQREL_1:5;
then [(f . 1),(f . 1)] in R1 \/ R2 by XBOOLE_0:def 3;
hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A12, A21; :: thesis: verum
end;
end;
end;
hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 ; :: thesis: verum
end;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A5, A6); :: thesis: verum
end;
hence [x,y] in R1 "\/" R2 by A2, A3; :: thesis: verum