theorem :: RFINSEQ2:32

for f being real-valued FinSequence st len f >= 1 holds
( max_p (sort_d f) = 1 & min_p (sort_a f) = 1 & (sort_d f) . 1 = max f & (sort_a f) . 1 = min f )