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