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 consider H being Function such that
A2: ( dom H = dom (sort_a h) & rng H = dom h & H is one-to-one & sort_a h = h * H ) by CLASSES1:85;
consider G being Function such that
A3: ( dom G = dom h & rng G = dom (sort_a h) & G is one-to-one & h = (sort_a h) * G ) by A1, CLASSES1:85;
thus ( h is one-to-one implies sort_a h is one-to-one ) by A2; :: thesis: ( sort_a h is one-to-one implies h is one-to-one )
thus ( sort_a h is one-to-one implies h is one-to-one ) by A3; :: thesis: verum