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 NUMBERS:19;
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) and
A5: rng H = dom hr and
A6: H is one-to-one and
A7: sort_a hr = hr * H by CLASSES1:77;
rng (sort_a hr) = rng hr by A3, CLASSES1:75;
then reconsider h4 = sort_a hr as FinSequence of NAT by FINSEQ_1:def 4;
A8: rng h = rng h4 by A5, A7, RELAT_1:28;
A9: 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 that
A10: 1 <= i and
A11: i < len h4 ; :: thesis: h4 . i < h4 . (i + 1)
A12: i + 1 <= len h4 by A11, NAT_1:13;
A13: i in dom h4 by A9, A10, A11, FINSEQ_1:1;
1 < i + 1 by A10, XREAL_1:29;
then A14: i + 1 in dom h4 by A9, A12, FINSEQ_1:1;
A15: h4 is one-to-one by A1, Th12;

A16: now :: thesis: not h4 . i = h4 . (i + 1)

assume h4 . i = h4 . (i + 1) ; :: thesis: contradiction
then i = i + 1 by A14, A13, A15, FUNCT_1:def 4;
hence contradiction ; :: thesis: verum

end;

h4 . i <= h4 . (i + 1) by A14, A13, INTEGRA2:def 1;
hence h4 . i < h4 . (i + 1) by A16, XXREAL_0:1; :: thesis: verum

end;

then A17: h4 is increasing ;
dom (sort_a hr) = dom hr by RFINSEQ2:31;
then reconsider H2 = H as Function of (dom h),(dom h) by A4, A5, FUNCT_2:1;
H2 is onto by A5, FUNCT_2:def 3;
then reconsider h5 = H as Permutation of (dom h) by A6;
A18: h4 = h * h5 by A7;
dom h = dom h5 by A2, FUNCT_2:def 1
.= dom h4 by A4 ;
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 A18, A17, A8; :: thesis: verum

end;

suppose A19: 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:42;
then reconsider h5 = h as Function of {},{} by A19, FUNCT_2:1;
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 A19, Th10; :: thesis: verum

end;

end;