let k be Nat; :: thesis: for p being XFinSequence holds mid p,1,k = p | k
let p be XFinSequence; :: thesis: mid p,1,k = p | k
1 -' 1 = 0 by XREAL_1:234;
hence mid p,1,k = p | k by Th19; :: thesis: verum