theorem Th29: :: SCMBSORT:44

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