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;
A1: 1 -' 1 = 0 by XREAL_1:234;
mid f,1,k2 = (f | k21) /^ (1 -' 1) by Def3;
hence mid f,1,k2 = f | k2 by A1, Th19; :: thesis: verum