let f be XFinSequence; :: thesis: for k2 being Element of NAT holds mid f,0 ,k2 = mid f,1,k2
let k2 be Element of NAT ; :: thesis: mid f,0 ,k2 = mid f,1,k2
reconsider k21 = k2 as Element of NAT ;
A1: 0 -' 1 = 0 by NAT_2:10;
A2: mid f,0 ,k2 = (f | k21) /^ (0 -' 1) by Def3;
mid f,1,k2 = f | k21 by Th25;
hence mid f,0 ,k2 = mid f,1,k2 by A2, A1, Th19; :: thesis: verum