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

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

hence
[x,y] in R1 "\/" R2
by A2, A3; :: thesis: verum
defpred S_{1}[ Nat] means ( 1 <= $1 & $1 <= len f implies [(f . 1),(f . $1)] in R1 "\/" R2 );

A5: S_{1}[ 0 ]
;

A6: for i being Nat st S_{1}[i] holds

S_{1}[i + 1]
_{1}[i]
from NAT_1:sch 2(A5, A6); :: thesis: verum

end;A5: S

A6: for i being Nat st S

S

proof

thus
for i being Nat holds S
let i be Nat; :: thesis: ( S_{1}[i] implies S_{1}[i + 1] )

assume A7: S_{1}[i]
; :: thesis: S_{1}[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;

end;assume A7: S

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 "\/" R2end;

hence
[(f . 1),(f . (i + 1))] in R1 "\/" R2
; :: thesis: verumper cases
( 1 <= i or 0 = i )
by A11;

end;

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

hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A7, A9, A13, EQREL_1:7, NAT_1:13; :: thesis: verum

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

then
[(f . i),(f . (i + 1))] in R1 "\/" R2
by A17, A18, EQREL_1:28;
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;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

hence [(f . 1),(f . (i + 1))] in R1 "\/" R2 by A7, A9, A13, EQREL_1:7, NAT_1:13; :: thesis: verum