let p be FinSequence; :: thesis: for n being Nat st n in dom p & n + 1 <= len p holds
mid (p,n,(n + 1)) = <*(p . n),(p . (n + 1))*>
let n be Nat; :: thesis: ( n in dom p & n + 1 <= len p implies mid (p,n,(n + 1)) = <*(p . n),(p . (n + 1))*> )
assume A1: ( n in dom p & n + 1 <= len p ) ; :: thesis: mid (p,n,(n + 1)) = <*(p . n),(p . (n + 1))*>
then n + 1 in dom p by FINSEQ_3:25, XREAL_1:31;
then A2: mid (p,(n + 1),(n + 1)) = <*(p . (n + 1))*> by Th7;
thus mid (p,n,(n + 1)) = <*(p . n)*> ^ (mid (p,(n + 1),(n + 1))) by A1, Th8, XREAL_1:29
.= <*(p . n),(p . (n + 1))*> by A2, FINSEQ_1:def 9 ; :: thesis: verum