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:10;
mid p,1,k = p | k by Th25;
hence mid p,0 ,k = mid p,1,k by A1, Th19; :: thesis: verum