:: deftheorem Def5 defines sort_d RFINSEQ2:def 5 :
for f being real-valued FinSequence
for b₂ being non-increasing FinSequence of REAL holds
( b₂ = sort_d f iff f,b₂ are_fiberwise_equipotent );