let p be XFinSequence; for k1, k2 being Nat st k1 > k2 holds
mid (p,k1,k2) = {}
let k1, k2 be Nat; ( k1 > k2 implies mid (p,k1,k2) = {} )
set k21 = k2;
A1:
len (p | k2) <= k2
by AFINSQ_1:55;
assume A2:
k1 > k2
; mid (p,k1,k2) = {}
then
k1 >= 0 + 1
by NAT_1:13;
then A3:
k1 -' 1 = k1 - 1
by XREAL_1:233;
k1 >= k2 + 1
by A2, NAT_1:13;
then
k1 - 1 >= (k2 + 1) - 1
by XREAL_1:9;
hence
mid (p,k1,k2) = {}
by A3, A1, Th6, XXREAL_0:2; verum