let Ke, Ne be Subset of NAT; :: thesis:
defpred S₁[ set , Function] means $1 = $2 . (min* (dom $2));
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 Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) );
A1: S₂[ {} ]

let Ne, Me be Subset of NAT; :: thesis:
let F be Function of Ne,Me; :: thesis:
assume that
A2: F = {} and
rng F is finite ; :: thesis:
reconsider R = rng F as empty set by A2;
set P = {} ;
A3: rng {} = {} ;
reconsider P = {} as Function of R,R by A3, FUNCT_2:1;
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 Nat st i in rng F & j in rng F & i < j holds
min* (F " {i}) < min* (F " {j}) ) ) ; :: thesis:

end;

A4: 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]

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

suppose rng F9 is empty ; :: thesis:

then F9 = {} ;
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 Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) by A1, A6; :: thesis:

end;

suppose A8: not rng F9 is empty ; :: thesis:

then reconsider domF = dom F as non empty Subset of NAT by A6, RELAT_1:42, XBOOLE_1:1;
reconsider K = K as non empty Subset of NAT by A6, A8;
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 3;

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

then (rng F) \ {(F . (min* domF))} = {} by Th54;
then A10: rng F = {(F . (min* domF))} by A9, ZFMISC_1:58;
A11: for i, j being Nat st i in rng F & j in rng F & i < j holds
min* (F " {i}) < min* (F " {j})

let i, j be Nat; :: thesis:
assume that
A12: i in rng F and
A13: j in rng F and
A14: i < j ; :: thesis:
i = F . (min* domF) by A10, A12, TARSKI:def 1;
hence min* (F " {i}) < min* (F " {j}) by A10, A13, A14, TARSKI:def 1; :: thesis:

end;

set P = id (rng F);
rng (id (rng F)) = rng F ;
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) by FUNCT_2:1;
then P * F = F by FUNCT_2:17;
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 Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) by A11; :: thesis:

end;

suppose A15: 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:70;
then reconsider rFD = rng (F | ((dom F) \ (F " {(F . (min* domF))}))) as non empty finite Subset of NAT by A7, A15, XBOOLE_1:1;
deffunc H₁( set ) -> set = F . (min* domF);
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:1;
A16: ( rFD is empty implies dFD is empty ) ;
reconsider rF = rng F as non empty finite Subset of NAT by A7, A9, XBOOLE_1:1;
A17: ( dFD c= N & rFD c= K ) ;
consider P being Permutation of (rng FD), G being Function of dFD,rFD such that
A18: FD = P * G and
A19: rng FD = rng G and
A20: for i, j being Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) by A5, A6, A9;
A21: for x being set st x in N \ dFD holds
H₁(x) in K by A9;
consider G2 being Function of N,K such that
A22: ( G2 | dFD = G & ( for x being set st x in N \ dFD holds
G2 . x = H₁(x) ) ) from STIRL2_1:sch 2(A21, A17, A16);
A23: rng G2 c= rng F

let Gx be object ; :: according to TARSKI:def 3 :: thesis:
assume Gx in rng G2 ; :: thesis:
then consider x being object such that
A24: x in dom G2 and
A25: G2 . x = Gx by FUNCT_1:def 3;
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 A22, A24, RELAT_1:61, 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 A19, A22, Th54, FUNCT_1:47, FUNCT_1:def 3, NAT_1:def 1;
hence Gx in rng F by A25, FUNCT_1:def 3, XBOOLE_0:def 5; :: thesis:

end;

A26: rng FD = (rng F) \ {(F . (min* domF))} by Th54;
dom FD = (dom F) /\ ((dom F) \ (F " {(F . (min* domF))})) by RELAT_1:61;
then A27: dFD = (dom F) \ (F " {(F . (min* domF))}) by XBOOLE_1:28, XBOOLE_1:36;
A28: F " {(F . (min* domF))} c= G2 " {(F . (min* domF))}

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A29: x in F " {(F . (min* domF))} ; :: thesis:
not x in (dom F) \ (F " {(F . (min* domF))}) by A29, XBOOLE_0:def 5;
then x in N \ dFD by A27, A29, XBOOLE_0:def 5;
then G2 . x = F . (min* domF) by A22;
then A30: G2 . x in {(F . (min* domF))} by TARSKI:def 1;
x in N by A29;
then x in dom G2 by FUNCT_2:def 1;
hence x in G2 " {(F . (min* domF))} by A30, FUNCT_1:def 7; :: thesis:

end;

rng F c= rng G2

rng FD = (rng F) \ {(F . (min* domF))} by Th54;
then A31: rng F = (rng FD) \/ {(F . (min* domF))} by A9, ZFMISC_1:116;
let Fx be object ; :: according to TARSKI:def 3 :: thesis:
assume A32: Fx in rng F ; :: thesis:

per cases by A32, A31, XBOOLE_0:def 3;

suppose A33: Fx in rng FD ; :: thesis:

rng (G2 | dFD) c= rng G2 by RELAT_1:70;
hence Fx in rng G2 by A19, A22, A33; :: thesis:

end;

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

A35: min* domF in dom F by NAT_1:def 1;
then min* domF in N ;
then min* domF in dom G2 by FUNCT_2:def 1;
then A36: G2 . (min* domF) in rng G2 by FUNCT_1:def 3;
F . (min* domF) in {(F . (min* domF))} by TARSKI:def 1;
then min* domF in F " {(F . (min* domF))} by A35, FUNCT_1:def 7;
then not min* domF in (dom F) \ (F " {(F . (min* domF))}) by XBOOLE_0:def 5;
then A37: min* domF in N \ dFD by A27, A35, XBOOLE_0:def 5;
Fx = F . (min* domF) by A34, TARSKI:def 1;
hence Fx in rng G2 by A22, A37, A36; :: thesis:

end;

end;

end;

hence Fx in rng G2 ; :: thesis:

end;

then A38: rng G2 = rng F by A23;
not F . (min* domF) in (rng F) \ {(F . (min* domF))} by ZFMISC_1:56;
then not F . (min* domF) in rng FD by Th54;
then consider P2 being Function of ((rng FD) \/ {(F . (min* domF))}),((rng FD) \/ {(F . (min* domF))}) such that
A39: P2 | (rng FD) = P and
A40: P2 . (F . (min* domF)) = F . (min* domF) by Th57;
not F . (min* domF) in (rng F) \ {(F . (min* domF))} by ZFMISC_1:56;
then A41: ( P2 is one-to-one & P2 is onto ) by A39, A40, A26, Th58;
(rng FD) \/ {(F . (min* domF))} = rng F by A9, A26, ZFMISC_1:116;
then reconsider P2 = P2 as Permutation of (rng F) by A41;
consider Orde being Function of rF,(Segm (card rF)) such that
A42: Orde is bijective and
A43: for n, k being Nat st n in dom Orde & k in dom Orde & n < k holds
Orde . n < Orde . k by Th59;
rng Orde = card rF by A42, FUNCT_2:def 3;
then reconsider Orde9 = Orde " as Function of (card rF),rF by A42, FUNCT_2:25;
consider P1 being Permutation of rF such that
A44: for k being 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, A42, A43, Lm5;
dom G2 = N by FUNCT_2:def 1;
then A45: G2 is Function of N,rF by A38, FUNCT_2:1;
reconsider P21 = P2 * (P1 ") as Function of rF,rF ;
reconsider P21 = P21 as Permutation of rF ;
dom P1 = rF by FUNCT_2:def 1;
then A46: (P1 ") * P1 = id rF by FUNCT_1:39;
rng (P1 * G2) c= K by XBOOLE_1:1;
then reconsider PG = P1 * G2 as Function of N,K by A45, FUNCT_2:6;
dom G2 = N by FUNCT_2:def 1;
then G2 is Function of N,rF by A38, FUNCT_2:1;
then (id rF) * G2 = G2 by FUNCT_2:17;
then A47: (P1 ") * (P1 * G2) = G2 by A46, RELAT_1:36;
G2 " {(F . (min* domF))} c= F " {(F . (min* domF))}

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

assume not x in N \ dFD ; :: thesis:
then ( ( x in dom G2 & dom G2 = N & not x in N ) or x in dFD ) by A48, XBOOLE_0:def 5;
then A50: x in dom G by FUNCT_2:def 1;
then A51: G . x in rng G by FUNCT_1:def 3;
A52: rng FD = (rng F) \ {(F . (min* domF))} by Th54;
G . x = G2 . x by A22, A50, FUNCT_1:47;
then not G2 . x in {(F . (min* domF))} by A51, A52, XBOOLE_0:def 5;
hence contradiction by A48, FUNCT_1:def 7; :: thesis:

end;

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

end;

then A54: G2 " {(F . (min* domF))} = F " {(F . (min* domF))} by A28;
A55: for n being Nat st n in rng FD holds
G " {n} = G2 " {n}

not K is empty ;
then dom F = N by FUNCT_2:def 1;
then A56: dFD = (dom G2) \ (G2 " {(F . (min* domF))}) by A27, A54, FUNCT_2:def 1;
A57: rng FD = (rng F) \ {(F . (min* domF))} by Th54;
let n be Nat; :: thesis:
assume n in rng FD ; :: thesis:
then not n in {(F . (min* domF))} by A57, XBOOLE_0:def 5;
then n <> F . (min* domF) by TARSKI:def 1;
hence G " {n} = G2 " {n} by A22, A56, Th54; :: thesis:

end;

A58: for i, j being Nat st i in rng PG & j in rng PG & i < j holds
min* (PG " {i}) < min* (PG " {j})

A59: for l being 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 )

A60: dom Orde = rF by FUNCT_2:def 1;
A61: Orde . (F . (min* domF)) in card rF ;
A62: Orde . (F . (min* domF)) < card rF by NAT_1:44;
let l be Nat; :: thesis:
assume that
A63: l in rF and
A64: l < F . (min* domF) ; :: thesis:
A65: Orde . l < Orde . (F . (min* domF)) by A9, A43, A63, A64, A60;
then (Orde . l) + 1 <= Orde . (F . (min* domF)) by NAT_1:13;
then A66: (Orde . l) + 1 < card rF by A62, XXREAL_0:2;
card rF = rng Orde by A42, FUNCT_2:def 3;
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 A65, A61, A66, FUNCT_2:def 1, NAT_1:13, NAT_1:44; :: thesis:

end;

A67: for n, k being Nat st n in dom Orde & k in dom Orde & Orde . n < Orde . k holds
n < k

let n, k be Nat; :: thesis:
assume that
A68: n in dom Orde and
A69: k in dom Orde and
A70: Orde . n < Orde . k ; :: thesis:
assume n >= k ; :: thesis:
then n > k by A70, XXREAL_0:1;
hence contradiction by A43, A68, A69, A70; :: thesis:

end;

A71: for n, k being Nat st n in rng Orde & k in rng Orde & n < k holds
Orde9 . n < Orde9 . k

let n, k be Nat; :: thesis:
assume that
A72: n in rng Orde and
A73: k in rng Orde ; :: thesis:
A74: n = Orde . (Orde9 . n) by A42, A72, FUNCT_1:35;
A75: dom Orde = rng Orde9 by A42, FUNCT_1:33;
A76: k = Orde . (Orde9 . k) by A42, A73, FUNCT_1:35;
assume A77: n < k ; :: thesis:
A78: rng Orde = dom Orde9 by A42, FUNCT_1:33;
then A79: Orde9 . n in dom Orde by A72, A75, FUNCT_1:def 3;
Orde9 . k in dom Orde by A73, A78, A75, FUNCT_1:def 3;
hence Orde9 . n < Orde9 . k by A67, A77, A74, A76, A79; :: thesis:

end;

rng FD = (rng F) \ {(F . (min* domF))} by Th54;
then A80: (rng FD) \/ {(F . (min* domF))} = rng G2 by A9, A38, ZFMISC_1:116;
let i, j be Nat; :: thesis:
assume that
A81: i in rng PG and
A82: j in rng PG and
A83: i < j ; :: thesis:
consider i1 being set such that
A84: i1 in dom P1 and
A85: i1 in rng G2 and
A86: P1 " {i} = {i1} and
A87: G2 " {i1} = PG " {i} by A81, Th61;
consider j1 being set such that
A88: j1 in dom P1 and
A89: j1 in rng G2 and
A90: P1 " {j} = {j1} and
A91: G2 " {j1} = PG " {j} by A82, Th61;
dom P1 = rF by FUNCT_2:def 1;
then reconsider i1 = i1, j1 = j1 as Element of NAT by A84, A88;
A92: i1 in P1 " {i} by A86, TARSKI:def 1;
then P1 . i1 in {i} by FUNCT_1:def 7;
then A93: P1 . i1 = i by TARSKI:def 1;
A94: j1 in P1 " {j} by A90, TARSKI:def 1;
then A95: P1 . j1 in {j} by FUNCT_1:def 7;
then A96: P1 . j1 = j by TARSKI:def 1;
A97: dom Orde = rF by FUNCT_2:def 1;

per cases by XXREAL_0:1;

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

A99: ( i1 in rng FD or i1 in {(F . (min* domF))} ) by A85, A80, XBOOLE_0:def 3;
then A100: G " {i1} = PG " {i} by A55, A87, A98, TARSKI:def 1;
A101: ( j1 in rng FD or j1 in {(F . (min* domF))} ) by A89, A80, XBOOLE_0:def 3;
i1 < j1

assume i1 >= j1 ; :: thesis:
then i1 > j1 by A83, A93, A96, XXREAL_0:1;
then Orde . i1 > Orde . j1 by A43, A92, A94, A97;
then A102: (Orde . i1) + 1 > (Orde . j1) + 1 by XREAL_1:8;
A103: (Orde . i1) + 1 in rng Orde by A84, A59, A98;
A104: Orde9 . ((Orde . j1) + 1) = j by A44, A94, A96, A98;
A105: (Orde . j1) + 1 in rng Orde by A88, A59, A98;
Orde9 . ((Orde . i1) + 1) = i by A44, A92, A93, A98;
hence contradiction by A83, A71, A102, A103, A105, A104; :: thesis:

end;

then min* (G " {i1}) < min* (G " {j1}) by A19, A20, A98, A99, A101, TARSKI:def 1;
hence min* (PG " {i}) < min* (PG " {j}) by A55, A91, A98, A101, A100, TARSKI:def 1; :: thesis:

end;

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

consider x being object such that
A107: x in dom G2 and
A108: G2 . x = j1 by A89, FUNCT_1:def 3;
G2 . x in {j1} by A108, TARSKI:def 1;
then PG " {j} is non empty Subset of NAT by A91, A107, FUNCT_1:def 7, XBOOLE_1:1;
then A109: min* (PG " {j}) in PG " {j} by NAT_1:def 1;
( j1 in rng FD or j1 in {(F . (min* domF))} ) by A89, A80, XBOOLE_0:def 3;
then A110: G " {j1} = PG " {j} by A55, A91, A106, TARSKI:def 1;
then min* (PG " {j}) in dom F by A27, A109, XBOOLE_0:def 5;
then A111: min* domF <= min* (PG " {j}) by NAT_1:def 1;
A112: min* domF in domF by NAT_1:def 1;
F . (min* domF) in {(F . (min* domF))} by TARSKI:def 1;
then A113: min* domF in F " {(F . (min* domF))} by A112, FUNCT_1:def 7;
then min* domF <> min* (PG " {j}) by A27, A110, A109, XBOOLE_0:def 5;
then A114: min* domF < min* (PG " {j}) by A111, XXREAL_0:1;
PG " {i} is Subset of NAT by XBOOLE_1:1;
then min* (PG " {i}) <= min* domF by A28, A87, A106, A113, NAT_1:def 1;
hence min* (PG " {i}) < min* (PG " {j}) by A114, XXREAL_0:2; :: thesis:

end;

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

card rF = rng Orde by A42, FUNCT_2:def 3;
then A116: 0 in rng Orde by NAT_1:44;
(Orde . i1) + 1 in rng Orde by A84, A59, A115;
then A117: Orde9 . ((Orde . i1) + 1) > Orde9 . 0 by A71, A116;
A118: P1 . j1 = Orde9 . 0 by A44, A94, A115;
Orde9 . ((Orde . i1) + 1) = i by A44, A92, A93, A115;
hence min* (PG " {i}) < min* (PG " {j}) by A83, A95, A117, A118, TARSKI:def 1; :: thesis:

end;

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

hence min* (PG " {i}) < min* (PG " {j}) by A83, A95, A93, TARSKI:def 1; :: thesis:

end;

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

A120: ( i1 in rng FD or i1 in {(F . (min* domF))} ) by A85, A80, XBOOLE_0:def 3;
then A121: G " {i1} = PG " {i} by A55, A87, A119, TARSKI:def 1;
A122: P1 . j1 = j1 by A44, A88, A119;
A123: ( j1 in rng FD or j1 in {(F . (min* domF))} ) by A89, A80, XBOOLE_0:def 3;
P1 . i1 = i1 by A44, A84, A119;
then min* (G " {i1}) < min* (G " {j1}) by A19, A20, A83, A93, A96, A119, A122, A120, A123, TARSKI:def 1;
hence min* (PG " {i}) < min* (PG " {j}) by A55, A91, A119, A123, A121, TARSKI:def 1; :: thesis:

end;

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

A125: dom Orde = rF by FUNCT_2:def 1;
rng (Orde ") = dom Orde by A42, FUNCT_1:33;
then consider x being object such that
A126: x in dom Orde9 and
A127: Orde9 . x = i1 by A84, A125, FUNCT_1:def 3;
A128: x in card rF by A126;
card rF is Subset of NAT by Th8;
then reconsider x = x as Element of NAT by A128;
P1 . i1 = i1 by A44, A84, A124;
then A129: Orde9 . x < Orde9 . 0 by A44, A83, A88, A93, A96, A124, A127;
A130: card rF = rng Orde by A42, FUNCT_2:def 3;
then 0 in rng Orde by NAT_1:44;
then x <= 0 by A71, A126, A130, A129;
hence min* (PG " {i}) < min* (PG " {j}) by A129; :: thesis:

end;

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

A132: ( i1 in rng FD or i1 in {(F . (min* domF))} ) by A85, A80, XBOOLE_0:def 3;
then A133: G " {i1} = PG " {i} by A55, A87, A131, TARSKI:def 1;
A134: ( j1 in rng FD or j1 in {(F . (min* domF))} ) by A89, A80, XBOOLE_0:def 3;
i1 < j1 by A131, XXREAL_0:2;
then min* (G " {i1}) < min* (G " {j1}) by A19, A20, A131, A132, A134, TARSKI:def 1;
hence min* (PG " {i}) < min* (PG " {j}) by A55, A91, A131, A134, A133, TARSKI:def 1; :: thesis:

end;

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

then dom Orde = rF by A88, A59;
then A136: Orde . (F . (min* domF)) in rng Orde by A9, FUNCT_1:def 3;
(Orde . j1) + 1 <= Orde . (F . (min* domF)) by A88, A59, A135;
then A137: ( (Orde . j1) + 1 < Orde . (F . (min* domF)) or (Orde . j1) + 1 = Orde . (F . (min* domF)) ) by XXREAL_0:1;
F . (min* domF) in dom Orde by A9, A88, A59, A135;
then A138: Orde9 . (Orde . (F . (min* domF))) = F . (min* domF) by A42, FUNCT_1:34;
A139: P1 . i1 = i1 by A44, A84, A135;
A140: Orde9 . ((Orde . j1) + 1) = P1 . j1 by A44, A88, A135;
(Orde . j1) + 1 in rng Orde by A88, A59, A135;
then P1 . j1 <= F . (min* domF) by A71, A137, A136, A138, A140;
hence min* (PG " {i}) < min* (PG " {j}) by A83, A93, A96, A135, A139, XXREAL_0:2; :: thesis:

end;

end;

end;

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

end;

not K is empty ;
then A141: dom F = N by FUNCT_2:def 1;
A142: for x being object st x in dom F holds
F . x = P2 . (G2 . x)

let x be object ; :: thesis:
assume A143: x in dom F ; :: thesis:

per cases by A143, XBOOLE_0:def 5;

suppose A144: x in N \ dFD ; :: thesis:

then A145: not x in (dom F) \ (F " {(F . (min* domF))}) by A27, XBOOLE_0:def 5;
x in dom F by A141, A144, XBOOLE_0:def 5;
then x in F " {(F . (min* domF))} by A145, XBOOLE_0:def 5;
then A146: F . x in {(F . (min* domF))} by FUNCT_1:def 7;
P2 . (G2 . x) = F . (min* domF) by A22, A40, A144;
hence F . x = P2 . (G2 . x) by A146, TARSKI:def 1; :: thesis:

end;

suppose A147: x in dFD ; :: thesis:

then A148: F . x = FD . x by FUNCT_1:47;
A149: FD . x = P . (G . x) by A18, A147, FUNCT_1:12;
A150: dom P = rng FD by FUNCT_2:def 1;
A151: x in dom G by A147, FUNCT_2:def 1;
then A152: G . x in rng FD by A19, FUNCT_1:def 3;
G . x = G2 . x by A22, A151, FUNCT_1:47;
hence F . x = P2 . (G2 . x) by A39, A148, A149, A152, A150, FUNCT_1:47; :: thesis:

end;

end;

end;

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

end;

A153: dom G2 = N by FUNCT_2:def 1;
for x being object holds
( x in dom F iff ( x in dom G2 & G2 . x in dom P2 ) )

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

assume A154: x in dom F ; :: thesis:
then dom P2 = rng F by A153, FUNCT_2:def 1;
hence ( x in dom G2 & G2 . x in dom P2 ) by A38, A153, A154, FUNCT_1:def 3; :: thesis:

end;

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

end;

then F = P2 * G2 by A142, FUNCT_1:10;
then A155: F = P21 * PG by A47, RELAT_1:36;
rng P1 = rF by FUNCT_2:def 3;
then rng (P1 * G2) = rF by A38, A45, FUNCT_2:14;
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 Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) by A155, A58; :: thesis:

end;

end;

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 Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) ; :: thesis:

end;

end;

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 Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) ) ) ; :: thesis:

end;

A156: for F being Function st rng F is finite holds
S₂[F] from STIRL2_1:sch 7(A1, A4);
let F be Function of Ne,Ke; :: thesis:
assume rng F is finite ; :: thesis:
then consider P being Permutation of (rng F), G being Function of Ne,Ke such that
A157: F = P * G and
A158: rng F = rng G and
A159: for i, j being Nat st i in rng G & j in rng G & i < j holds
min* (G " {i}) < min* (G " {j}) by A156;
G is 'increasing by A159;
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 A157, A158; :: thesis: