let h be FinSequence of NAT ; :: thesis: ( h is one-to-one implies ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 ) )
assume A1: h is one-to-one ; :: thesis: ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 )

per cases ( dom h <> {} or dom h = {} ) ;

suppose A2: dom h <> {} ; :: thesis: ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 )

rng h c= REAL by XBOOLE_1:1;
then reconsider hr = h as FinSequence of REAL by FINSEQ_1:def 4;
A3: hr, sort_a hr are_fiberwise_equipotent by RFINSEQ2:def 6;
then consider H being Function such that
A4: ( dom H = dom (sort_a hr) & rng H = dom hr & H is one-to-one & sort_a hr = hr * H ) by CLASSES1:85;
dom (sort_a hr) = dom hr by RFINSEQ2:31;
then reconsider H2 = H as Function of (dom h),(dom h) by A4, FUNCT_2:3;
H2 is onto by A4, FUNCT_2:def 3;
then reconsider h5 = H as Permutation of (dom h) by A4;
rng (sort_a hr) = rng hr by A3, CLASSES1:83;
then reconsider h4 = sort_a hr as FinSequence of NAT by FINSEQ_1:def 4;
A5: h4 = h * h5 by A4;
A6: dom h4 = Seg (len h4) by FINSEQ_1:def 3;
for i being Nat st 1 <= i & i < len h4 holds
h4 . i < h4 . (i + 1)

proof

let i be Nat; :: thesis: ( 1 <= i & i < len h4 implies h4 . i < h4 . (i + 1) )
assume A7: ( 1 <= i & i < len h4 ) ; :: thesis: h4 . i < h4 . (i + 1)
then A8: 1 < i + 1 by XREAL_1:31;
i + 1 <= len h4 by A7, NAT_1:13;
then A9: i + 1 in dom h4 by A8, A6, FINSEQ_1:3;
A10: i in dom h4 by A7, A6, FINSEQ_1:3;
then A11: h4 . i <= h4 . (i + 1) by A9, INTEGRA2:def 1;
A12: h4 is one-to-one by Th16, A1;

now

assume h4 . i = h4 . (i + 1) ; :: thesis: contradiction
then i = i + 1 by A12, A9, A10, FUNCT_1:def 8;
hence contradiction ; :: thesis: verum

end;

hence h4 . i < h4 . (i + 1) by A11, XXREAL_0:1; :: thesis: verum

end;

then A13: h4 is increasing by Def2;
A14: dom h = dom h5 by A2, FUNCT_2:def 1
.= dom h4 by A4 ;
rng h = rng h4 by A4, RELAT_1:47;
hence ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 ) by A13, A14, A5; :: thesis: verum

end;

suppose A15: dom h = {} ; :: thesis: ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 )

then rng h = {} by RELAT_1:65;
then reconsider h5 = h as Function of {} ,{} by A15, FUNCT_2:3;
reconsider h22 = h * h5 as FinSequence of NAT ;
h22 is increasing ;
hence ex h3 being Permutation of (dom h) ex h2 being FinSequence of NAT st
( h2 = h * h3 & h2 is increasing & dom h = dom h2 & rng h = rng h2 ) by A15, Th14; :: thesis: verum

end;

end;