let Ke, Ne be Subset of NAT; :: thesis: for F being Function of Ne,Ke st rng F is finite holds
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 )

defpred S1[ set , Function] means \$1 = \$2 . (min* (dom \$2));
defpred S2[ 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: S2[ {} ]
proof
let Ne, Me be Subset of NAT; :: thesis: for F being Function of Ne,Me st F = {} & rng F is finite holds
ex P being Permutation of (rng F) ex G being Function of Ne,Me 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}) ) )

let F be Function of Ne,Me; :: thesis: ( F = {} & rng F is finite implies ex P being Permutation of (rng F) ex G being Function of Ne,Me 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}) ) ) )

assume that
A2: F = {} and
rng F is finite ; :: thesis: ex P being Permutation of (rng F) ex G being Function of Ne,Me 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}) ) )

reconsider R = rng F as empty set by A2;
set P = {} ;
A3: rng {} = {} ;
reconsider P = {} as Function of R,R by ;
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: ex G being Function of Ne,Me 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}) ) )

take F ; :: thesis: ( 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}) ) )

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: verum
end;
A4: for F being Function st ( for x being set st x in rng F & S1[x,F] holds
S2[F | ((dom F) \ (F " {x}))] ) holds
S2[F]
proof
let F9 be Function; :: thesis: ( ( for x being set st x in rng F9 & S1[x,F9] holds
S2[F9 | ((dom F9) \ (F9 " {x}))] ) implies S2[F9] )

assume A5: for x being set st x in rng F9 & S1[x,F9] holds
S2[F9 | ((dom F9) \ (F9 " {x}))] ; :: thesis: S2[F9]
let N, K be Subset of NAT; :: thesis: for F being Function of N,K st F = F9 & rng F is finite holds
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}) ) )

let F be Function of N,K; :: thesis: ( F = F9 & rng F is finite implies 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}) ) ) )

assume that
A6: F = F9 and
A7: rng F is finite ; :: thesis: 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}) ) )

now :: thesis: 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}) ) )
per cases ( rng F9 is empty or not rng F9 is empty ) ;
suppose rng F9 is empty ; :: thesis: 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}) ) )

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: verum
end;
suppose A8: not rng F9 is empty ; :: thesis: 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}) ) )

then reconsider domF = dom F as non empty Subset of NAT by ;
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;
now :: thesis: 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}) ) )
per cases ( rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty or not rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty ) ;
suppose rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty ; :: thesis: 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}) ) )

then (rng F) \ {(F . (min* domF))} = {} by Th54;
then A10: rng F = {(F . (min* domF))} by ;
A11: for i, j being Nat st i in rng F & j in rng F & i < j holds
min* (F " {i}) < min* (F " {j})
proof
let i, j be Nat; :: thesis: ( i in rng F & j in rng F & i < j implies min* (F " {i}) < min* (F " {j}) )
assume that
A12: i in rng F and
A13: j in rng F and
A14: i < j ; :: thesis: min* (F " {i}) < min* (F " {j})
i = F . (min* domF) by ;
hence min* (F " {i}) < min* (F " {j}) by ; :: thesis: verum
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: verum
end;
suppose A15: not rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty ; :: thesis: 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}) ) )

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 ;
deffunc H1( 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 ;
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
H1(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 = H1(x) ) ) from A23: rng G2 c= rng F
proof
let Gx be object ; :: according to TARSKI:def 3 :: thesis: ( not Gx in rng G2 or Gx in rng F )
assume Gx in rng G2 ; :: thesis: Gx in rng F
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 ;
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 ;
hence Gx in rng F by ; :: thesis: verum
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 ;
A28: F " {(F . (min* domF))} c= G2 " {(F . (min* domF))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in F " {(F . (min* domF))} or x in G2 " {(F . (min* domF))} )
assume A29: x in F " {(F . (min* domF))} ; :: thesis: x in G2 " {(F . (min* domF))}
not x in (dom F) \ (F " {(F . (min* domF))}) by ;
then x in N \ dFD by ;
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 ; :: thesis: verum
end;
rng F c= rng G2
proof
rng FD = (rng F) \ {(F . (min* domF))} by Th54;
then A31: rng F = (rng FD) \/ {(F . (min* domF))} by ;
let Fx be object ; :: according to TARSKI:def 3 :: thesis: ( not Fx in rng F or Fx in rng G2 )
assume A32: Fx in rng F ; :: thesis: Fx in rng G2
now :: thesis: Fx in rng G2
per cases ( Fx in rng FD or Fx in {(F . (min* domF))} ) by ;
suppose A33: Fx in rng FD ; :: thesis: Fx in rng G2
rng (G2 | dFD) c= rng G2 by RELAT_1:70;
hence Fx in rng G2 by ; :: thesis: verum
end;
suppose A34: Fx in {(F . (min* domF))} ; :: thesis: Fx in rng G2
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 ;
then not min* domF in (dom F) \ (F " {(F . (min* domF))}) by XBOOLE_0:def 5;
then A37: min* domF in N \ dFD by ;
Fx = F . (min* domF) by ;
hence Fx in rng G2 by ; :: thesis: verum
end;
end;
end;
hence Fx in rng G2 ; :: thesis: verum
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 ;
(rng FD) \/ {(F . (min* domF))} = rng F by ;
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 ;
then reconsider Orde9 = Orde " as Function of (card rF),rF by ;
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 ;
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 ;
dom G2 = N by FUNCT_2:def 1;
then G2 is Function of N,rF by ;
then (id rF) * G2 = G2 by FUNCT_2:17;
then A47: (P1 ") * (P1 * G2) = G2 by ;
G2 " {(F . (min* domF))} c= F " {(F . (min* domF))}
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in G2 " {(F . (min* domF))} or x in F " {(F . (min* domF))} )
assume A48: x in G2 " {(F . (min* domF))} ; :: thesis: x in F " {(F . (min* domF))}
A49: x in N \ dFD
proof
assume not x in N \ dFD ; :: thesis: contradiction
then ( ( x in dom G2 & dom G2 = N & not x in N ) or x in dFD ) by ;
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 ;
then not G2 . x in {(F . (min* domF))} by ;
hence contradiction by A48, FUNCT_1:def 7; :: thesis: verum
end;
then A53: not x in (dom F) \ (F " {(F . (min* domF))}) by ;
dom F = N by ;
then x in dom F by ;
hence x in F " {(F . (min* domF))} by ; :: thesis: verum
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}
proof
not K is empty ;
then dom F = N by FUNCT_2:def 1;
then A56: dFD = (dom G2) \ (G2 " {(F . (min* domF))}) by ;
A57: rng FD = (rng F) \ {(F . (min* domF))} by Th54;
let n be Nat; :: thesis: ( n in rng FD implies G " {n} = G2 " {n} )
assume n in rng FD ; :: thesis: G " {n} = G2 " {n}
then not n in {(F . (min* domF))} by ;
then n <> F . (min* domF) by TARSKI:def 1;
hence G " {n} = G2 " {n} by ; :: thesis: verum
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})
proof
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 )
proof
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: ( l in rF & l < F . (min* domF) implies ( (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 ) )
assume that
A63: l in rF and
A64: l < F . (min* domF) ; :: thesis: ( (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 )
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 ;
card rF = rng Orde by ;
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 ; :: thesis: verum
end;
A67: for n, k being Nat st n in dom Orde & k in dom Orde & Orde . n < Orde . k holds
n < k
proof
let n, k be Nat; :: thesis: ( n in dom Orde & k in dom Orde & Orde . n < Orde . k implies n < k )
assume that
A68: n in dom Orde and
A69: k in dom Orde and
A70: Orde . n < Orde . k ; :: thesis: n < k
assume n >= k ; :: thesis: contradiction
then n > k by ;
hence contradiction by A43, A68, A69, A70; :: thesis: verum
end;
A71: for n, k being Nat st n in rng Orde & k in rng Orde & n < k holds
Orde9 . n < Orde9 . k
proof
let n, k be Nat; :: thesis: ( n in rng Orde & k in rng Orde & n < k implies Orde9 . n < Orde9 . k )
assume that
A72: n in rng Orde and
A73: k in rng Orde ; :: thesis: ( not n < k or Orde9 . n < Orde9 . k )
A74: n = Orde . (Orde9 . n) by ;
A75: dom Orde = rng Orde9 by ;
A76: k = Orde . (Orde9 . k) by ;
assume A77: n < k ; :: thesis: Orde9 . n < Orde9 . k
A78: rng Orde = dom Orde9 by ;
then A79: Orde9 . n in dom Orde by ;
Orde9 . k in dom Orde by ;
hence Orde9 . n < Orde9 . k by A67, A77, A74, A76, A79; :: thesis: verum
end;
rng FD = (rng F) \ {(F . (min* domF))} by Th54;
then A80: (rng FD) \/ {(F . (min* domF))} = rng G2 by ;
let i, j be Nat; :: thesis: ( i in rng PG & j in rng PG & i < j implies min* (PG " {i}) < min* (PG " {j}) )
assume that
A81: i in rng PG and
A82: j in rng PG and
A83: i < j ; :: thesis: min* (PG " {i}) < min* (PG " {j})
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 ;
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 ;
dom P1 = rF by FUNCT_2:def 1;
then reconsider i1 = i1, j1 = j1 as Element of NAT by ;
A92: i1 in P1 " {i} by ;
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 ;
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;
now :: thesis: min* (PG " {i}) < min* (PG " {j})
per cases ( ( i1 < F . (min* domF) & j1 < F . (min* domF) ) or ( i1 = F . (min* domF) & j1 <> F . (min* domF) ) or ( i1 < F . (min* domF) & j1 = F . (min* domF) ) or ( i1 = F . (min* domF) & j1 = F . (min* domF) ) or ( i1 > F . (min* domF) & j1 > F . (min* domF) ) or ( i1 > F . (min* domF) & j1 = F . (min* domF) ) or ( i1 < F . (min* domF) & j1 > F . (min* domF) ) or ( i1 > F . (min* domF) & j1 < F . (min* domF) ) ) by XXREAL_0:1;
suppose A98: ( i1 < F . (min* domF) & j1 < F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
A99: ( i1 in rng FD or i1 in {(F . (min* domF))} ) by ;
then A100: G " {i1} = PG " {i} by ;
A101: ( j1 in rng FD or j1 in {(F . (min* domF))} ) by ;
i1 < j1
proof
assume i1 >= j1 ; :: thesis: contradiction
then i1 > j1 by ;
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 ;
A104: Orde9 . ((Orde . j1) + 1) = j by A44, A94, A96, A98;
A105: (Orde . j1) + 1 in rng Orde by ;
Orde9 . ((Orde . i1) + 1) = i by A44, A92, A93, A98;
hence contradiction by A83, A71, A102, A103, A105, A104; :: thesis: verum
end;
then min* (G " {i1}) < min* (G " {j1}) by ;
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
suppose A106: ( i1 = F . (min* domF) & j1 <> F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
consider x being object such that
A107: x in dom G2 and
A108: G2 . x = j1 by ;
G2 . x in {j1} by ;
then PG " {j} is non empty Subset of NAT by ;
then A109: min* (PG " {j}) in PG " {j} by NAT_1:def 1;
( j1 in rng FD or j1 in {(F . (min* domF))} ) by ;
then A110: G " {j1} = PG " {j} by ;
then min* (PG " {j}) in dom F by ;
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 ;
then min* domF <> min* (PG " {j}) by ;
then A114: min* domF < min* (PG " {j}) by ;
PG " {i} is Subset of NAT by XBOOLE_1:1;
then min* (PG " {i}) <= min* domF by ;
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
suppose A115: ( i1 < F . (min* domF) & j1 = F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
card rF = rng Orde by ;
then A116: 0 in rng Orde by NAT_1:44;
(Orde . i1) + 1 in rng Orde by ;
then A117: Orde9 . ((Orde . i1) + 1) > Orde9 . 0 by ;
A118: P1 . j1 = Orde9 . 0 by ;
Orde9 . ((Orde . i1) + 1) = i by ;
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
suppose ( i1 = F . (min* domF) & j1 = F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
suppose A119: ( i1 > F . (min* domF) & j1 > F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
A120: ( i1 in rng FD or i1 in {(F . (min* domF))} ) by ;
then A121: G " {i1} = PG " {i} by ;
A122: P1 . j1 = j1 by ;
A123: ( j1 in rng FD or j1 in {(F . (min* domF))} ) by ;
P1 . i1 = i1 by ;
then min* (G " {i1}) < min* (G " {j1}) by ;
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
suppose A124: ( i1 > F . (min* domF) & j1 = F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
A125: dom Orde = rF by FUNCT_2:def 1;
rng (Orde ") = dom Orde by ;
then consider x being object such that
A126: x in dom Orde9 and
A127: Orde9 . x = i1 by ;
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 ;
then A129: Orde9 . x < Orde9 . 0 by A44, A83, A88, A93, A96, A124, A127;
A130: card rF = rng Orde by ;
then 0 in rng Orde by NAT_1:44;
then x <= 0 by ;
hence min* (PG " {i}) < min* (PG " {j}) by A129; :: thesis: verum
end;
suppose A131: ( i1 < F . (min* domF) & j1 > F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
A132: ( i1 in rng FD or i1 in {(F . (min* domF))} ) by ;
then A133: G " {i1} = PG " {i} by ;
A134: ( j1 in rng FD or j1 in {(F . (min* domF))} ) by ;
i1 < j1 by ;
then min* (G " {i1}) < min* (G " {j1}) by ;
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
suppose A135: ( i1 > F . (min* domF) & j1 < F . (min* domF) ) ; :: thesis: min* (PG " {i}) < min* (PG " {j})
then dom Orde = rF by ;
then A136: Orde . (F . (min* domF)) in rng Orde by ;
(Orde . j1) + 1 <= Orde . (F . (min* domF)) by ;
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 ;
A139: P1 . i1 = i1 by ;
A140: Orde9 . ((Orde . j1) + 1) = P1 . j1 by ;
(Orde . j1) + 1 in rng Orde by ;
then P1 . j1 <= F . (min* domF) by ;
hence min* (PG " {i}) < min* (PG " {j}) by ; :: thesis: verum
end;
end;
end;
hence min* (PG " {i}) < min* (PG " {j}) ; :: thesis: verum
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)
proof
let x be object ; :: thesis: ( x in dom F implies F . x = P2 . (G2 . x) )
assume A143: x in dom F ; :: thesis: F . x = P2 . (G2 . x)
now :: thesis: F . x = P2 . (G2 . x)
per cases ( x in N \ dFD or x in dFD ) by ;
suppose A144: x in N \ dFD ; :: thesis: F . x = P2 . (G2 . x)
then A145: not x in (dom F) \ (F " {(F . (min* domF))}) by ;
x in dom F by ;
then x in F " {(F . (min* domF))} by ;
then A146: F . x in {(F . (min* domF))} by FUNCT_1:def 7;
P2 . (G2 . x) = F . (min* domF) by ;
hence F . x = P2 . (G2 . x) by ; :: thesis: verum
end;
suppose A147: x in dFD ; :: thesis: F . x = P2 . (G2 . x)
then A148: F . x = FD . x by FUNCT_1:47;
A149: FD . x = P . (G . x) by ;
A150: dom P = rng FD by FUNCT_2:def 1;
A151: x in dom G by ;
then A152: G . x in rng FD by ;
G . x = G2 . x by ;
hence F . x = P2 . (G2 . x) by ; :: thesis: verum
end;
end;
end;
hence F . x = P2 . (G2 . x) ; :: thesis: verum
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 ) )
proof
let x be object ; :: thesis: ( x in dom F iff ( x in dom G2 & G2 . x in dom P2 ) )
thus ( x in dom F implies ( x in dom G2 & G2 . x in dom P2 ) ) :: thesis: ( x in dom G2 & G2 . x in dom P2 implies x in dom F )
proof
assume A154: x in dom F ; :: thesis: ( x in dom G2 & G2 . x in dom P2 )
then dom P2 = rng F by ;
hence ( x in dom G2 & G2 . x in dom P2 ) by ; :: thesis: verum
end;
thus ( x in dom G2 & G2 . x in dom P2 implies x in dom F ) by A141; :: thesis: verum
end;
then F = P2 * G2 by ;
then A155: F = P21 * PG by ;
rng P1 = rF by FUNCT_2:def 3;
then rng (P1 * G2) = rF by ;
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 ; :: thesis: verum
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: verum
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: verum
end;
A156: for F being Function st rng F is finite holds
S2[F] from let F be Function of Ne,Ke; :: thesis: ( rng F is finite implies 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 ) )

assume rng F is finite ; :: thesis: 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 )

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 ; :: thesis: verum