let h be FinSequence of REAL ; :: thesis: ( h is one-to-one iff sort_a h is one-to-one )
A1: h, sort_a h are_fiberwise_equipotent by RFINSEQ2:def 6;
then ex H being Function st
( dom H = dom (sort_a h) & rng H = dom h & H is one-to-one & sort_a h = h * H ) by CLASSES1:77;
hence ( h is one-to-one implies sort_a h is one-to-one ) ; :: thesis: ( sort_a h is one-to-one implies h is one-to-one )
ex G being Function st
( dom G = dom h & rng G = dom (sort_a h) & G is one-to-one & h = (sort_a h) * G ) by A1, CLASSES1:77;
hence ( sort_a h is one-to-one implies h is one-to-one ) ; :: thesis: verum