theorem Th28: :: SCMISORT:35

for w being FinSequence of INT holds Initialized ((fsloc 0) .--> w) is Insert-Sort-Algorithm -autonomic