theorem Th19: :: SCMISORT:26

for f being FinSeq-Location holds UsedI*Loc (insert-sort f) = {f}