let k be Nat; :: thesis: for p being XFinSequence holds mid (p,0,k) = mid (p,1,k)
let p be XFinSequence; :: thesis: mid (p,0,k) = mid (p,1,k)
A1: 0 -' 1 = 0 by NAT_2:8;
mid (p,1,k) = p | k by Th16;
hence mid (p,0,k) = mid (p,1,k) by A1, Th10; :: thesis: verum