for P being Instruction-Sequence of SCMPDS
for s being 0 -started State of SCMPDS
for f, g being FinSequence of INT
for p0, n being Nat st p0 >= 6 & len f = n & len g = n & f is_FinSequence_on s,p0 & g is_FinSequence_on IExec ((insert-sort (n,(p0 + 1))),P,s),p0 holds
( f,g are_fiberwise_equipotent & g is_non_decreasing_on 1,n )