theorem Th18: :: SCMISORT:25

for f being FinSeq-Location holds UsedILoc (insert-sort f) = {(intloc 0),(intloc 1),(intloc 2),(intloc 3),(intloc 4),(intloc 5),(intloc 6)}