let f be XFinSequence; :: thesis: for k2 being Nat holds mid f,1,k2 = f | k2
let k2 be Nat; :: thesis: mid f,1,k2 = f | k2
reconsider k21 = k2 as Element of NAT by ORDINAL1:def 13;
A2: mid f,1,k2 = (f | k21) /^ (1 -' 1) by AB540b;
1 -' 1 = 0 by XREAL_1:234;
hence mid f,1,k2 = f | k2 by A2, Th31; :: thesis: verum