:: deftheorem defines smid FINSEQ_8:def 1 :
for f being FinSequence
for k1, k2 being Nat holds smid (f,k1,k2) = (f /^ (k1 -' 1)) | ((k2 + 1) -' k1);