let f be FinSequence; :: thesis: for k1, k2 being Nat st k1 > k2 holds
smid (f,k1,k2) = {}
let k1, k2 be Nat; :: thesis: ( k1 > k2 implies smid (f,k1,k2) = {} )
assume A1: k1 > k2 ; :: thesis: smid (f,k1,k2) = {}
set g = f /^ (k1 -' 1);
k2 + 1 <= k1 by A1, NAT_1:13;
then smid (f,k1,k2) = (f /^ (k1 -' 1)) | 0 by NAT_2:8;
hence smid (f,k1,k2) = {} ; :: thesis: verum