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