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 S_{1}[ set , Function] means $1 = $2 . (min* (dom $2));

defpred S_{2}[ 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_{2}[ {} ]
_{1}[x,F] holds

S_{2}[F | ((dom F) \ (F " {x}))] ) holds

S_{2}[F]

S_{2}[F]
from STIRL2_1:sch 7(A1, A4);

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

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 S

defpred S

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

proof

A4:
for F being Function st ( for x being set st x in rng F & S
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 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: 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;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 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: 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

S

S

proof

A156:
for F being Function st rng F is finite holds
let F9 be Function; :: thesis: ( ( for x being set st x in rng F9 & S_{1}[x,F9] holds

S_{2}[F9 | ((dom F9) \ (F9 " {x}))] ) implies S_{2}[F9] )

assume A5: for x being set st x in rng F9 & S_{1}[x,F9] holds

S_{2}[F9 | ((dom F9) \ (F9 " {x}))]
; :: thesis: S_{2}[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}) ) )

( 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;S

assume A5: for x being set st x in rng F9 & S

S

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}) ) )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}) ) )

per cases
( rng F9 is empty or not rng F9 is empty )
;

end;

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}) ) )

( 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;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

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}) ) )

( 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 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;

( 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;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}) ) )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}) ) )

per cases
( rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty or not rng (F | ((dom F) \ (F " {(F . (min* domF))}))) is empty )
;

end;

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}) ) )

( 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 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})

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;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})

proof

set P = id (rng F);
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 A10, A12, TARSKI:def 1;

hence min* (F " {i}) < min* (F " {j}) by A10, A13, A14, TARSKI:def 1; :: thesis: verum

end;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 A10, A12, TARSKI:def 1;

hence min* (F " {i}) < min* (F " {j}) by A10, A13, A14, TARSKI:def 1; :: thesis: verum

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

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}) ) )

( 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 A7, A15, XBOOLE_1:1;

deffunc H_{1}( 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_{1}(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_{1}(x) ) )
from STIRL2_1:sch 2(A21, A17, A16);

A23: rng G2 c= rng F

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))}

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))}

A55: for n being Nat st n in rng FD holds

G " {n} = G2 " {n}

min* (PG " {i}) < min* (PG " {j})

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)

for x being object holds

( x in dom F iff ( x in dom G2 & G2 . x in dom P2 ) )

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

end;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

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

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

A23: rng G2 c= rng F

proof

A26:
rng FD = (rng F) \ {(F . (min* domF))}
by Th54;
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 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: verum

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

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))}

proof

rng F c= rng G2
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 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: verum

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

proof

then A38:
rng G2 = rng F
by A23;
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: ( not Fx in rng F or Fx in rng G2 )

assume A32: Fx in rng F ; :: thesis: Fx in rng G2

end;then A31: rng F = (rng FD) \/ {(F . (min* domF))} by A9, ZFMISC_1:116;

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 G2end;

hence
Fx in rng G2
; :: thesis: verumper cases
( Fx in rng FD or Fx in {(F . (min* domF))} )
by A32, A31, XBOOLE_0:def 3;

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

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

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))}

proof

then A54:
G2 " {(F . (min* domF))} = F " {(F . (min* domF))}
by A28;
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

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

end;assume A48: x in G2 " {(F . (min* domF))} ; :: thesis: x in F " {(F . (min* domF))}

A49: x in N \ dFD

proof

then A53:
not x in (dom F) \ (F " {(F . (min* domF))})
by A27, XBOOLE_0:def 5;
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 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: verum

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

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

A55: for n being Nat st n in rng FD holds

G " {n} = G2 " {n}

proof

A58:
for i, j being Nat st i in rng PG & j in rng PG & i < j holds
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: ( 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 A57, XBOOLE_0:def 5;

then n <> F . (min* domF) by TARSKI:def 1;

hence G " {n} = G2 " {n} by A22, A56, Th54; :: thesis: verum

end;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: ( 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 A57, XBOOLE_0:def 5;

then n <> F . (min* domF) by TARSKI:def 1;

hence G " {n} = G2 " {n} by A22, A56, Th54; :: thesis: verum

min* (PG " {i}) < min* (PG " {j})

proof

not K is empty
;
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 )

n < k

Orde9 . n < Orde9 . k

then A80: (rng FD) \/ {(F . (min* domF))} = rng G2 by A9, A38, ZFMISC_1:116;

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 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;

end;( (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

A67:
for n, k being Nat st n in dom Orde & k in dom Orde & Orde . n < Orde . k holds
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 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: verum

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

n < k

proof

A71:
for n, k being Nat st n in rng Orde & k in rng Orde & n < k holds
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 A70, XXREAL_0:1;

hence contradiction by A43, A68, A69, A70; :: thesis: verum

end;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 A70, XXREAL_0:1;

hence contradiction by A43, A68, A69, A70; :: thesis: verum

Orde9 . n < Orde9 . k

proof

rng FD = (rng F) \ {(F . (min* domF))}
by Th54;
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 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: Orde9 . n < Orde9 . k

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

end;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 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: Orde9 . n < Orde9 . k

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

then A80: (rng FD) \/ {(F . (min* domF))} = rng G2 by A9, A38, ZFMISC_1:116;

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 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;

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

hence
min* (PG " {i}) < min* (PG " {j})
; :: thesis: verumper 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;

end;

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 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

hence min* (PG " {i}) < min* (PG " {j}) by A55, A91, A98, A101, A100, TARSKI:def 1; :: thesis: verum

end;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

proof

then
min* (G " {i1}) < min* (G " {j1})
by A19, A20, A98, A99, A101, TARSKI:def 1;
assume
i1 >= j1
; :: thesis: contradiction

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

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

hence min* (PG " {i}) < min* (PG " {j}) by A55, A91, A98, A101, A100, TARSKI:def 1; :: thesis: verum

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

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

suppose A115:
( i1 < F . (min* domF) & j1 = F . (min* domF) )
; :: thesis: min* (PG " {i}) < min* (PG " {j})

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

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

suppose
( i1 = F . (min* domF) & j1 = F . (min* domF) )
; :: thesis: min* (PG " {i}) < min* (PG " {j})

end;

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

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

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

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

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

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

suppose A135:
( i1 > F . (min* domF) & j1 < F . (min* domF) )
; :: thesis: min* (PG " {i}) < min* (PG " {j})

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

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

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

A153:
dom G2 = N
by FUNCT_2:def 1;
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)

end;assume A143: x in dom F ; :: thesis: F . x = P2 . (G2 . x)

now :: thesis: F . x = P2 . (G2 . x)end;

hence
F . x = P2 . (G2 . x)
; :: thesis: verumper cases
( x in N \ dFD or x in dFD )
by A143, XBOOLE_0:def 5;

end;

suppose A144:
x in N \ dFD
; :: thesis: F . x = P2 . (G2 . x)

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

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

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

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

for x being object holds

( x in dom F iff ( x in dom G2 & G2 . x in dom P2 ) )

proof

then
F = P2 * G2
by A142, FUNCT_1:10;
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 )

end;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

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

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

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

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

( 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

( 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

S

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