theorem :: FINSEQ_8:29

for f being FinSequence
for k1, k2 being Nat st k1 in dom f & k2 in dom f holds
smid (f,k1,k2) = (k1,k2) -cut f