:: deftheorem Def6 defines sort_a RFINSEQ2:def 6 :
for f being FinSequence of REAL
for b₂ being non-decreasing FinSequence of REAL holds
( b₂ = sort_a f iff f,b₂ are_fiberwise_equipotent );