let p be FinSequence; for n being Nat st n in dom p & n + 2 <= len p holds
mid (p,n,(n + 2)) = <*(p . n),(p . (n + 1)),(p . (n + 2))*>
let n be Nat; ( n in dom p & n + 2 <= len p implies mid (p,n,(n + 2)) = <*(p . n),(p . (n + 1)),(p . (n + 2))*> )
assume A1:
( n in dom p & n + 2 <= len p )
; mid (p,n,(n + 2)) = <*(p . n),(p . (n + 1)),(p . (n + 2))*>
then A2:
( 1 <= n & (n + 1) + 1 <= len p )
by FINSEQ_3:25;
A3:
1 <= n + 1
by XREAL_1:31;
((n + 1) + 1) - 1 <= (len p) - 0
by A1, XREAL_1:13;
then A5:
n + 1 in dom p
by A3, FINSEQ_3:25;
A6:
mid (p,(n + 1),(n + 2)) = <*(p . (n + 1)),(p . (n + 2))*>
by A2, A5, Th9;
thus mid (p,n,(n + 2)) =
<*(p . n)*> ^ (mid (p,(n + 1),(n + 2)))
by A1, Th8, XREAL_1:29
.=
<*(p . n)*> ^ (<*(p . (n + 1))*> ^ <*(p . (n + 2))*>)
by A6, FINSEQ_1:def 9
.=
(<*(p . n)*> ^ <*(p . (n + 1))*>) ^ <*(p . (n + 2))*>
by FINSEQ_1:32
.=
<*(p . n),(p . (n + 1)),(p . (n + 2))*>
by FINSEQ_1:def 10
; verum