theorem Th23: :: SCMISORT:30

for f being FinSeq-Location
for k being Nat st k < 71 holds
k in dom (insert-sort f)