let f be XFinSequence; :: thesis: for k1, k2 being Nat st k1 > k2 holds
mid f,k1,k2 = {}
let k1, k2 be Nat; :: thesis: ( k1 > k2 implies mid f,k1,k2 = {} )
reconsider k11 = k1, k21 = k2 as Element of NAT by ORDINAL1:def 13;
A1: len (f | k21) <= k21 by Th13;
assume A2: k1 > k2 ; :: thesis: mid f,k1,k2 = {}
then k1 >= 0 + 1 by NAT_1:13;
then A3: k1 -' 1 = k1 - 1 by XREAL_1:235;
k1 >= k2 + 1 by A2, NAT_1:13;
then A4: k1 - 1 >= (k2 + 1) - 1 by XREAL_1:11;
mid f,k1,k2 = (f | k21) /^ (k11 -' 1) by Def3;
hence mid f,k1,k2 = {} by A3, A4, A1, Th15, XXREAL_0:2; :: thesis: verum