let Ne, Ke be Subset of NAT ; :: thesis:
defpred S₁[ set ] means for Ne, Ke being Subset of NAT
for F being Function of Ne,Ke st F = $1 & rng F is finite holds
ex P being Permutation of (rng F) ex G being Function of Ne,Ke st
( F = P * G & rng F = rng G & ( for i, j being Element of NAT st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) );
A1: S₁[ {} ]

proof

let Ne, Me be Subset of NAT ; :: thesis:
let F be Function of Ne,Me; :: thesis:
assume A2: ( F = {} & rng F is finite ) ; :: thesis:
reconsider R = rng F as empty set by A2;
set P = {} ;
( rng {} = {} & dom {} = {} ) ;
then reconsider P = {} as Function of R,R by FUNCT_2:3;
( dom P = {} & rng R = {} ) ;
then ( P is one-to-one & P is onto ) by FUNCT_2:def 3;
then reconsider P = P as Permutation of (rng F) ;
take P ; :: thesis:
take F ; :: thesis:
rng F = R ;
then F = {} ;
hence ( F = P * F & rng F = rng F & ( for i, j being Element of NAT st i in rng F & j in rng F & i < j holds
min* (F " {i}) < min* (F " {j}) ) ) ; :: thesis:

end;

defpred S₂[ set , Function] means $1 = $2 . (min* (dom $2));
A5: for F being Function st ( for x being set st x in rng F & S₂[x,F] holds
S₁[F | ((dom F) \ (F " {x}))] ) holds
S₁[F]

proof

let F' be Function; :: thesis:
assume A6: for x being set st x in rng F' & S₂[x,F'] holds
S₁[F' | ((dom F') \ (F' " {x}))] ; :: thesis:
let N, K be Subset of NAT ; :: thesis:
let F be Function of N,K; :: thesis:
assume A7: ( F = F' & rng F is finite ) ; :: thesis:

now

per cases ;

suppose rng F' is empty ; :: thesis:

then F' = {} ;
hence ex P being Permutation of (rng F) ex G being Function of N,K st
( F = P * G & rng F = rng G & ( for i, j being Element of NAT st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) by A1, A7; :: thesis:

end;

suppose A8: not rng F' is empty ; :: thesis:

then reconsider K = K as non empty Subset of NAT by A7;
reconsider domF = dom F as non empty Subset of NAT by A7, A8, RELAT_1:65, XBOOLE_1:1;
set m = min* domF;
set D = (dom F) \ (F " {(F . (min* domF))});
min* domF in domF by NAT_1:def 1;
then A9: F . (min* domF) in rng F by FUNCT_1:def 5;

now

per cases ;

suppose rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty ; :: thesis:

then (rng F) \ {(F . (min* domF))} = {} by Th64;
then A10: rng F = {(F . (min* domF))} by A9, ZFMISC_1:66;
set P = id (rng F);
rng (id (rng F)) = rng F by RELAT_1:71;
then ( id (rng F) is one-to-one & id (rng F) is onto ) by FUNCT_2:def 3;
then reconsider P = id (rng F) as Permutation of (rng F) ;
( F is Function of (dom F),(rng F) & rng F <> 0 ) by A9, FUNCT_2:3;
then A11: P * F = F by FUNCT_2:23;
for i, j being Element of NAT st i in rng F & j in rng F & i < j holds
min* (F " {i}) < min* (F " {j})

proof

let i, j be Element of NAT ; :: thesis:
assume A12: ( i in rng F & j in rng F & i < j ) ; :: thesis:
( i = F . (min* domF) & j = F . (min* domF) ) by A10, A12, TARSKI:def 1;
hence min* (F " {i}) < min* (F " {j}) by A12; :: thesis:

end;

hence ex P being Permutation of (rng F) ex G being Function of N,K st
( F = P * G & rng F = rng G & ( for i, j being Element of NAT st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) by A11; :: thesis:

end;

suppose A13: not rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty ; :: thesis:

rng (F | ((dom F) \ (F " {(F . (min* domF))}))) c= rng F by RELAT_1:99;
then reconsider rFD = rng (F | ((dom F) \ (F " {(F . (min* domF))}))) as non empty finite Subset of NAT by A7, A13, XBOOLE_1:1;
reconsider rF = rng F as non empty finite Subset of NAT by A7, A9, XBOOLE_1:1;
reconsider dFD = dom (F | ((dom F) \ (F " {(F . (min* domF))}))) as Subset of NAT by XBOOLE_1:1;
reconsider FD = F | ((dom F) \ (F " {(F . (min* domF))})) as Function of dFD,rFD by FUNCT_2:3;
A14: dFD = (dom F) \ (F " {(F . (min* domF))})

proof

( dFD = dom FD & dom FD = (dom F) /\ ((dom F) \ (F " {(F . (min* domF))})) & (dom F) \ (F " {(F . (min* domF))}) c= dom F ) by RELAT_1:90, XBOOLE_1:36;
hence dFD = (dom F) \ (F " {(F . (min* domF))}) by XBOOLE_1:28; :: thesis:

end;

consider P being Permutation of (rng FD), G being Function of dFD,rFD such that
A15: ( FD = P * G & rng FD = rng G ) and
A16: for i, j being Element of NAT st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) by A6, A7, A9;
consider Orde being Function of rF,(card rF) such that
A17: Orde is bijective and
A18: for n, k being Element of NAT st n in dom Orde & k in dom Orde & n < k holds
Orde . n < Orde . k by Th69;
( Orde is one-to-one & rng Orde = card rF ) by A17, FUNCT_2:def 3;
then reconsider Orde' = Orde " as Function of (card rF),rF by FUNCT_2:31;
consider P1 being Permutation of rF such that
A19: for k being Element of NAT st k in rF holds
( ( k < F . (min* domF) implies P1 . k = (Orde " ) . ((Orde . k) + 1) ) & ( k = F . (min* domF) implies P1 . k = (Orde " ) . 0 ) & ( k > F . (min* domF) implies P1 . k = k ) ) by A9, A17, A18, Lm4;
deffunc H₁( set ) -> Element of NAT = F . (min* domF);
A20: for x being set st x in N \ dFD holds
H₁(x) in K by A9;
A21: ( dFD c= N & rFD c= K ) ;
A22: ( rFD is empty implies dFD is empty ) ;
consider G2 being Function of N,K such that
A23: ( G2 | dFD = G & ( for x being set st x in N \ dFD holds
G2 . x = H₁(x) ) ) from STIRL2_1:sch 2(A20, A21, A22);
not F . (min* domF) in (rng F) \ {(F . (min* domF))} by ZFMISC_1:64;
then not F . (min* domF) in rng FD by Th64;
then consider P2 being Function of ((rng FD) \/ {(F . (min* domF))}),((rng FD) \/ {(F . (min* domF))}) such that
A24: ( P2 | (rng FD) = P & P2 . (F . (min* domF)) = F . (min* domF) ) by Th67;
( P is one-to-one & P is onto & rng FD = (rng F) \ {(F . (min* domF))} & not F . (min* domF) in (rng F) \ {(F . (min* domF))} ) by Th64, ZFMISC_1:64;
then ( P2 is one-to-one & P2 is onto & (rng FD) \/ {(F . (min* domF))} = rng F ) by A9, A24, Th68, ZFMISC_1:140;
then reconsider P2 = P2 as Permutation of (rng F) ;
A25: rng G2 c= rng F

proof

let Gx be set ; :: according to TARSKI:def 3 :: thesis:
assume A26: Gx in rng G2 ; :: thesis:
consider x being set such that
A27: ( x in dom G2 & G2 . x = Gx ) by A26, FUNCT_1:def 5;
dom G2 = N by FUNCT_2:def 1;
then ((dom G2) /\ dFD) \/ (N \ dFD) = dom G2 by XBOOLE_1:51;
then ( ( dom G = (dom G2) /\ dFD & x in (dom G2) /\ dFD ) or x in N \ dFD ) by A23, A27, RELAT_1:90, XBOOLE_0:def 3;
then ( ( G . x in rng FD & G . x = G2 . x & rng FD = (rng F) \ {(F . (min* domF))} ) or ( G2 . x = F . (min* domF) & min* domF in domF ) ) by A15, A23, Th64, FUNCT_1:70, FUNCT_1:def 5, NAT_1:def 1;
hence Gx in rng F by A27, FUNCT_1:def 5, XBOOLE_0:def 5; :: thesis:

end;

rng F c= rng G2

proof

let Fx be set ; :: according to TARSKI:def 3 :: thesis:
assume A28: Fx in rng F ; :: thesis:
rng FD = (rng F) \ {(F . (min* domF))} by Th64;
then A29: rng F = (rng FD) \/ {(F . (min* domF))} by A9, ZFMISC_1:140;

now

per cases by A28, A29, XBOOLE_0:def 3;

suppose Fx in rng FD ; :: thesis:

then ( Fx in rng G & rng (G2 | dFD) c= rng G2 ) by A15, RELAT_1:99;
hence Fx in rng G2 by A23; :: thesis:

end;

suppose A30: Fx in {(F . (min* domF))} ; :: thesis:

( min* domF in dom F & F . (min* domF) in {(F . (min* domF))} & not K is empty ) by NAT_1:def 1, TARSKI:def 1;
then ( min* domF in F " {(F . (min* domF))} & dom F = N ) by FUNCT_1:def 13, FUNCT_2:def 1;
then ( not min* domF in (dom F) \ (F " {(F . (min* domF))}) & min* domF in N & N = dom G2 ) by FUNCT_2:def 1, XBOOLE_0:def 5;
then ( min* domF in N \ dFD & Fx = F . (min* domF) & min* domF in dom G2 ) by A14, A30, TARSKI:def 1, XBOOLE_0:def 5;
then ( G2 . (min* domF) = Fx & G2 . (min* domF) in rng G2 ) by A23, FUNCT_1:def 5;
hence Fx in rng G2 ; :: thesis:

end;

hence Fx in rng G2 ; :: thesis:

end;

then A31: rng G2 = rng F by A25, XBOOLE_0:def 10;
A32: F = P2 * G2

proof

not K is empty ;
then A33: ( dom F = N & dom G2 = N ) by FUNCT_2:def 1;
A34: for x being set holds
( x in dom F iff ( x in dom G2 & G2 . x in dom P2 ) )

proof

let x be set ; :: thesis:
thus ( x in dom F implies ( x in dom G2 & G2 . x in dom P2 ) ) :: thesis:

proof

assume x in dom F ; :: thesis:
then ( x in dom G2 & dom P2 = rng F ) by A33, FUNCT_2:def 1;
hence ( x in dom G2 & G2 . x in dom P2 ) by A31, FUNCT_1:def 5; :: thesis:

end;

thus ( x in dom G2 & G2 . x in dom P2 implies x in dom F ) by A33; :: thesis:

end;

for x being set st x in dom F holds
F . x = P2 . (G2 . x)

proof

let x be set ; :: thesis:
assume A35: x in dom F ; :: thesis:

now

per cases by A35, XBOOLE_0:def 5;

suppose x in N \ dFD ; :: thesis:

then A36: ( P2 . (G2 . x) = F . (min* domF) & x in dom F & not x in (dom F) \ (F " {(F . (min* domF))}) ) by A14, A23, A24, A33, XBOOLE_0:def 5;
then x in F " {(F . (min* domF))} by XBOOLE_0:def 5;
then F . x in {(F . (min* domF))} by FUNCT_1:def 13;
hence F . x = P2 . (G2 . x) by A36, TARSKI:def 1; :: thesis:

end;

suppose x in dFD ; :: thesis:

then ( x in dom FD & x in dom G ) by FUNCT_2:def 1;
then ( F . x = FD . x & G . x = G2 . x & FD . x = P . (G . x) & G . x in rng FD & dom P = rng FD ) by A15, A23, FUNCT_1:22, FUNCT_1:70, FUNCT_1:def 5, FUNCT_2:def 1;
hence F . x = P2 . (G2 . x) by A24, FUNCT_1:70; :: thesis:

end;

hence F . x = P2 . (G2 . x) ; :: thesis:

end;

hence F = P2 * G2 by A34, FUNCT_1:20; :: thesis:

end;

A37: G2 " {(F . (min* domF))} = F " {(F . (min* domF))}

proof

thus G2 " {(F . (min* domF))} c= F " {(F . (min* domF))} :: according to XBOOLE_0:def 10 :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A38: x in G2 " {(F . (min* domF))} ; :: thesis:
x in N \ dFD

proof

assume not x in N \ dFD ; :: thesis:
then ( ( x in dom G2 & dom G2 = N & not x in N ) or x in dFD ) by A38, XBOOLE_0:def 5;
then x in dom G by FUNCT_2:def 1;
then ( G . x in rng G & G . x = G2 . x ) by A23, FUNCT_1:70, FUNCT_1:def 5;
then ( G2 . x in rng FD & rng FD = (rng F) \ {(F . (min* domF))} ) by Th64;
then not G2 . x in {(F . (min* domF))} by XBOOLE_0:def 5;
hence contradiction by A38, FUNCT_1:def 13; :: thesis:

end;

then ( x in N \ ((dom F) \ (F " {(F . (min* domF))})) & dom F = N ) by A9, A14, FUNCT_2:def 1;
then ( x in dom F & not x in (dom F) \ (F " {(F . (min* domF))}) ) by XBOOLE_0:def 5;
hence x in F " {(F . (min* domF))} by XBOOLE_0:def 5; :: thesis:

end;

thus F " {(F . (min* domF))} c= G2 " {(F . (min* domF))} :: thesis:

proof

let x be set ; :: according to TARSKI:def 3 :: thesis:
assume A39: x in F " {(F . (min* domF))} ; :: thesis:
( not x in (dom F) \ (F " {(F . (min* domF))}) & dom F = N ) by A9, A39, FUNCT_2:def 1, XBOOLE_0:def 5;
then ( x in N \ dFD & x in N ) by A14, A39, XBOOLE_0:def 5;
then ( G2 . x = F . (min* domF) & x in dom G2 ) by A23, FUNCT_2:def 1;
then ( G2 . x in {(F . (min* domF))} & x in dom G2 ) by TARSKI:def 1;
hence x in G2 " {(F . (min* domF))} by FUNCT_1:def 13; :: thesis:

end;

A40: for n being Element of NAT st n in rng FD holds
G " {n} = G2 " {n}

proof

let n be Element of NAT ; :: thesis:
assume A41: n in rng FD ; :: thesis:
not K is empty ;
then ( dFD = (dom F) \ (F " {(F . (min* domF))}) & dom F = N & dom G2 = N & rng FD = (rng F) \ {(F . (min* domF))} ) by A14, Th64, FUNCT_2:def 1;
then ( dFD = (dom G2) \ (G2 " {(F . (min* domF))}) & not n in {(F . (min* domF))} ) by A37, A41, XBOOLE_0:def 5;
then ( G2 | ((dom G2) \ (G2 " {(F . (min* domF))})) = G & n <> F . (min* domF) ) by A23, TARSKI:def 1;
hence G " {n} = G2 " {n} by Th64; :: thesis:

end;

reconsider P21 = P2 * (P1 " ) as Function of rF,rF ;
reconsider P21 = P21 as Permutation of rF ;
dom G2 = N by FUNCT_2:def 1;
then ( G2 is Function of N,rF & rng P1 = rF & rng G2 = rF ) by A31, FUNCT_2:3, FUNCT_2:def 3;
then A42: ( P1 * G2 is Function of N,rF & rng (P1 * G2) c= K & rng (P1 * G2) = rF ) by FUNCT_2:20, XBOOLE_1:1;
then reconsider PG = P1 * G2 as Function of N,K by FUNCT_2:8;
dom G2 = N by FUNCT_2:def 1;
then ( G2 is Function of N,rF & dom P1 = rF ) by A31, FUNCT_2:3, FUNCT_2:def 1;
then ( (id rF) * G2 = G2 & (P1 " ) * P1 = id rF ) by FUNCT_1:61, FUNCT_2:23;
then (P1 " ) * (P1 * G2) = G2 by RELAT_1:55;
then A43: F = P21 * PG by A32, RELAT_1:55;
for i, j being Element of NAT st i in rng PG & j in rng PG & i < j holds
min* (PG " {i}) < min* (PG " {j})

proof

let i, j be Element of NAT ; :: thesis:
assume A44: ( i in rng PG & j in rng PG & i < j ) ; :: thesis:
consider i1 being set such that
A45: ( i1 in dom P1 & i1 in rng G2 & P1 " {i} = {i1} & G2 " {i1} = PG " {i} ) by A44, Th71;
consider j1 being set such that
A46: ( j1 in dom P1 & j1 in rng G2 & P1 " {j} = {j1} & G2 " {j1} = PG " {j} ) by A44, Th71;
dom P1 = rF by FUNCT_2:def 1;
then reconsider i1 = i1, j1 = j1 as Element of NAT by A45, A46;
( rng FD = (rng F) \ {(F . (min* domF))} & not F . (min* domF) in (rng F) \ {(F . (min* domF))} ) by Th64, ZFMISC_1:64;
then A47: (rng FD) \/ {(F . (min* domF))} = rng G2 by A9, A31, ZFMISC_1:140;
A48: for n, k being Element of NAT st n in dom Orde & k in dom Orde & Orde . n < Orde . k holds
n < k

proof

let n, k be Element of NAT ; :: thesis:
assume A49: ( n in dom Orde & k in dom Orde & Orde . n < Orde . k ) ; :: thesis:
assume n >= k ; :: thesis:
then n > k by A49, XXREAL_0:1;
hence contradiction by A18, A49; :: thesis:

end;

A50: for n, k being Element of NAT st n in rng Orde & k in rng Orde & n < k holds
Orde' . n < Orde' . k

proof

let n, k be Element of NAT ; :: thesis:
assume A51: ( n in rng Orde & k in rng Orde ) ; :: thesis:
assume A52: n < k ; :: thesis:
( rng Orde = dom Orde' & dom Orde = rng Orde' & rng Orde = card rF ) by A17, FUNCT_1:55, FUNCT_2:def 3;
then ( n = Orde . (Orde' . n) & k = Orde . (Orde' . k) & Orde' . k in dom Orde & Orde' . n in dom Orde & dom Orde is Subset of NAT ) by A51, A17, FUNCT_1:57, FUNCT_1:def 5, XBOOLE_1:1;
hence Orde' . n < Orde' . k by A48, A52; :: thesis:

end;

( i1 in P1 " {i} & j1 in P1 " {j} ) by A45, A46, TARSKI:def 1;
then A54: ( i1 in dom P1 & P1 . i1 in {i} & j1 in dom P1 & P1 . j1 in {j} & dom P1 = rF & ( card rF = {} implies rF = {} ) ) by FUNCT_1:def 13, FUNCT_2:def 1;
then A55: ( P1 . i1 = i & P1 . j1 = j & i1 in rF & j1 in rF & dom Orde = rF ) by FUNCT_2:def 1, TARSKI:def 1;
A56: for l being Element of NAT st l in rF & l < F . (min* domF) holds
( (Orde . l) + 1 in rng Orde & (Orde . l) + 1 is Element of NAT & (Orde . l) + 1 <= Orde . (F . (min* domF)) & Orde . (F . (min* domF)) is Element of NAT & dom Orde = rF )

proof

let l be Element of NAT ; :: thesis:
assume A57: ( l in rF & l < F . (min* domF) ) ; :: thesis:
A58: ( dom Orde = rF & card rF = rng Orde ) by A17, FUNCT_2:def 1, FUNCT_2:def 3;
then A59: ( Orde . l < Orde . (F . (min* domF)) & Orde . (F . (min* domF)) in card rF & card rF is Subset of NAT ) by A9, A18, A57, Th8;
then ( (Orde . l) + 1 <= Orde . (F . (min* domF)) & Orde . (F . (min* domF)) < card rF & Orde . (F . (min* domF)) is Element of NAT ) by NAT_1:13, NAT_1:45;
then (Orde . l) + 1 < card rF by XXREAL_0:2;
hence ( (Orde . l) + 1 in rng Orde & (Orde . l) + 1 is Element of NAT & (Orde . l) + 1 <= Orde . (F . (min* domF)) & Orde . (F . (min* domF)) is Element of NAT & dom Orde = rF ) by A58, A59, NAT_1:13, NAT_1:45; :: thesis:

end;

now

per cases by XXREAL_0:1;

suppose A60: ( i1 < F . (min* domF) & j1 < F . (min* domF) ) ; :: thesis:

i1 < j1

proof

assume i1 >= j1 ; :: thesis:
then i1 > j1 by A44, A55, XXREAL_0:1;
then Orde . i1 > Orde . j1 by A18, A55;
then ( (Orde . i1) + 1 > (Orde . j1) + 1 & (Orde . i1) + 1 in rng Orde & (Orde . j1) + 1 in rng Orde & (Orde . i1) + 1 is Element of NAT & (Orde . j1) + 1 is Element of NAT ) by A45, A46, A56, A60, XREAL_1:10;
then ( Orde' . ((Orde . i1) + 1) > Orde' . ((Orde . j1) + 1) & Orde' . ((Orde . i1) + 1) = i & Orde' . ((Orde . j1) + 1) = j ) by A19, A50, A55, A60;
hence contradiction by A44; :: thesis:

end;

then ( i1 < j1 & ( i1 in rng FD or i1 in {(F . (min* domF))} ) & not i1 in {(F . (min* domF))} & ( j1 in rng FD or j1 in {(F . (min* domF))} ) & not j1 in {(F . (min* domF))} ) by A45, A46, A47, A60, TARSKI:def 1, XBOOLE_0:def 3;
then ( min* (G " {i1}) < min* (G " {j1}) & G " {i1} = PG " {i} & G " {j1} = PG " {j} ) by A15, A16, A40, A45, A46;
hence min* (PG " {i}) < min* (PG " {j}) ; :: thesis:

end;

suppose A61: ( i1 = F . (min* domF) & j1 <> F . (min* domF) ) ; :: thesis:

then ( ( j1 in rng FD or j1 in {(F . (min* domF))} ) & not j1 in {(F . (min* domF))} & F . (min* domF) in {(F . (min* domF))} & min* domF in domF ) by A46, A47, NAT_1:def 1, TARSKI:def 1, XBOOLE_0:def 3;
then A62: ( min* domF in F " {(F . (min* domF))} & F " {(F . (min* domF))} = PG " {i} & G " {j1} = PG " {j} & PG " {i} is Subset of NAT & G " {j1} c= dom G & dFD = (dom F) \ (F " {(F . (min* domF))}) ) by A14, A37, A40, A45, A46, A61, FUNCT_1:def 13, RELAT_1:167, XBOOLE_1:1;
consider x being set such that
A63: ( x in dom G2 & G2 . x = j1 ) by A46, FUNCT_1:def 5;
G2 . x in {j1} by A63, TARSKI:def 1;
then PG " {j} is non empty Subset of NAT by A46, A63, FUNCT_1:def 13, XBOOLE_1:1;
then min* (PG " {j}) in PG " {j} by NAT_1:def 1;
then ( min* (PG " {j}) in dom F & not min* (PG " {j}) in F " {(F . (min* domF))} & min* domF in F " {(F . (min* domF))} ) by A62, XBOOLE_0:def 5;
then ( min* domF <= min* (PG " {j}) & min* domF <> min* (PG " {j}) ) by NAT_1:def 1;
then ( min* domF < min* (PG " {j}) & min* (PG " {i}) <= min* domF ) by A62, NAT_1:def 1, XXREAL_0:1;
hence min* (PG " {i}) < min* (PG " {j}) by XXREAL_0:2; :: thesis:

end;

suppose A64: ( i1 < F . (min* domF) & j1 = F . (min* domF) ) ; :: thesis:

( i1 in rF & card rF > 0 & card rF = rng Orde ) by A17, A45, FUNCT_2:def 3;
then ( (Orde . i1) + 1 > 0 & (Orde . i1) + 1 in rng Orde & (Orde . i1) + 1 is Element of NAT & 0 in rng Orde ) by A56, A64, NAT_1:45;
then ( Orde' . ((Orde . i1) + 1) > Orde' . 0 & P1 . j1 = Orde' . 0 & Orde' . ((Orde . i1) + 1) = i ) by A19, A50, A55, A64;
hence min* (PG " {i}) < min* (PG " {j}) by A44, A54, TARSKI:def 1; :: thesis:

end;

suppose ( i1 = F . (min* domF) & j1 = F . (min* domF) ) ; :: thesis:

hence min* (PG " {i}) < min* (PG " {j}) by A44, A55; :: thesis:

end;

suppose ( i1 > F . (min* domF) & j1 > F . (min* domF) ) ; :: thesis:

then ( P1 . i1 = i1 & P1 . j1 = j1 & ( i1 in rng FD or i1 in {(F . (min* domF))} ) & not i1 in {(F . (min* domF))} & ( j1 in rng FD or j1 in {(F . (min* domF))} ) & not j1 in {(F . (min* domF))} ) by A19, A45, A46, A47, TARSKI:def 1, XBOOLE_0:def 3;
then ( min* (G " {i1}) < min* (G " {j1}) & G " {i1} = PG " {i} & G " {j1} = PG " {j} ) by A15, A16, A40, A44, A45, A46, A55;
hence min* (PG " {i}) < min* (PG " {j}) ; :: thesis:

end;

suppose ( i1 > F . (min* domF) & j1 = F . (min* domF) ) ; :: thesis:

then A65: ( P1 . i1 = i1 & P1 . j1 = (Orde " ) . 0 ) by A19, A45, A46;
( rng (Orde " ) = dom Orde & dom (Orde " ) = rng Orde & rng Orde = card rF & dom Orde = rF & i1 in rF ) by A45, A17, FUNCT_1:55, FUNCT_2:def 1, FUNCT_2:def 3;
then consider x being set such that
A66: ( x in dom Orde' & Orde' . x = i1 ) by FUNCT_1:def 5;
( x in card rF & card rF is Subset of NAT ) by A66, Th8;
then reconsider x = x as Element of NAT ;
( card rF > 0 & card rF = rng Orde ) by A17, FUNCT_2:def 3;
then ( 0 in rng Orde & x in rng Orde & Orde' . x < Orde' . 0 ) by A44, A55, A65, A66, NAT_1:45;
then ( x <= 0 & Orde' . x <> Orde' . 0 ) by A50;
hence min* (PG " {i}) < min* (PG " {j}) ; :: thesis:

end;

suppose ( i1 < F . (min* domF) & j1 > F . (min* domF) ) ; :: thesis:

then ( i1 < j1 & ( i1 in rng FD or i1 in {(F . (min* domF))} ) & not i1 in {(F . (min* domF))} & ( j1 in rng FD or j1 in {(F . (min* domF))} ) & not j1 in {(F . (min* domF))} ) by A45, A46, A47, TARSKI:def 1, XBOOLE_0:def 3, XXREAL_0:2;
then ( min* (G " {i1}) < min* (G " {j1}) & G " {i1} = PG " {i} & G " {j1} = PG " {j} ) by A15, A16, A40, A45, A46;
hence min* (PG " {i}) < min* (PG " {j}) ; :: thesis:

end;

suppose A67: ( i1 > F . (min* domF) & j1 < F . (min* domF) ) ; :: thesis:

then ( (Orde . j1) + 1 in rng Orde & (Orde . j1) + 1 is Element of NAT & (Orde . j1) + 1 <= Orde . (F . (min* domF)) & Orde . (F . (min* domF)) is Element of NAT & dom Orde = rF ) by A46, A56;
then ( (Orde . j1) + 1 in rng Orde & (Orde . j1) + 1 is Element of NAT & ( (Orde . j1) + 1 < Orde . (F . (min* domF)) or (Orde . j1) + 1 = Orde . (F . (min* domF)) ) & Orde . (F . (min* domF)) is Element of NAT & Orde . (F . (min* domF)) in rng Orde & F . (min* domF) in dom Orde & Orde is one-to-one & j1 in rF ) by A9, A17, A46, FUNCT_1:def 5, XXREAL_0:1;
then ( ( Orde' . ((Orde . j1) + 1) < Orde' . (Orde . (F . (min* domF))) or Orde' . ((Orde . j1) + 1) = Orde' . (Orde . (F . (min* domF))) ) & Orde' . (Orde . (F . (min* domF))) = F . (min* domF) & Orde' . ((Orde . j1) + 1) = P1 . j1 ) by A19, A50, A67, FUNCT_1:56;
then ( P1 . j1 <= F . (min* domF) & P1 . i1 = i1 ) by A19, A45, A67;
hence min* (PG " {i}) < min* (PG " {j}) by A44, A55, A67, XXREAL_0:2; :: thesis:

end;

hence min* (PG " {i}) < min* (PG " {j}) ; :: thesis:

end;

A68: for F being Function st rng F is finite holds
S₁[F] from STIRL2_1:sch 9(A1, A5);
let F be Function of Ne,Ke; :: thesis:
assume A69: rng F is finite ; :: thesis:
consider P being Permutation of (rng F), G being Function of Ne,Ke such that
A70: ( F = P * G & rng F = rng G & ( for i, j being Element of NAT st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) by A68, A69;
G is "increasing by A70, Def5;
hence ex I being Function of Ne,Ke ex P being Permutation of (rng F) st
( F = P * I & rng F = rng I & I is "increasing ) by A70; :: thesis: