:: deftheorem Def7 defines Sorting-Function SCMFSA_M:def 7 :
for b₁ being PartFunc of (FinPartSt SCM+FSA),(FinPartSt SCM+FSA) holds
( b₁ = Sorting-Function iff for p, q being FinPartState of SCM+FSA holds
( [p,q] in b₁ iff ex t being FinSequence of INT ex u being FinSequence of REAL st
( t,u are_fiberwise_equipotent & u is FinSequence of INT & u is non-increasing & p = (fsloc 0) .--> t & q = (fsloc 0) .--> u ) ) );