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