for s being State of SCM+FSA
for f being FinSeq-Location
for p being Instruction-Sequence of SCM+FSA
for S being State of SCM+FSA st S = IExec ((Selection-sort f),p,s) holds
( S . f is_non_decreasing_on 1, len (S . f) & ex p being Permutation of (dom (s . f)) st S . f = (s . f) * p )