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:232;
hence mid (p,1,k) = p | k by Th10; :: thesis: verum