let Ke, Ne, Me be Subset of NAT; :: thesis: for F being Function of Ne,Ke st rng F is finite holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

defpred S_{1}[ set , Function] means $1 = $2 . (min* (dom $2));

defpred S_{2}[ set ] means for Ne, Ke, Me being Subset of NAT

for F being Function of Ne,Ke st F = $1 holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 );

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, A8);

hence for F being Function of Ne,Ke st rng F is finite holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 ) ; :: thesis: verum

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

defpred S

defpred S

for F being Function of Ne,Ke st F = $1 holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 );

A1: S

proof

A8:
for F being Function st ( for x being set st x in rng F & S
let Ne, Ke, Me be Subset of NAT; :: thesis: for F being Function of Ne,Ke st F = {} holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let F be Function of Ne,Ke; :: thesis: ( F = {} implies for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 ) )

assume A2: F = {} ; :: thesis: for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let I1, I2 be Function of Ne,Me; :: thesis: for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let P1, P2 be Function; :: thesis: ( P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing implies ( P1 = P2 & I1 = I2 ) )

assume that

P1 is one-to-one and

P2 is one-to-one and

A3: rng I1 = rng I2 and

A4: rng I1 = dom P1 and

A5: dom P1 = dom P2 and

A6: F = P1 * I1 and

F = P2 * I2 and

I1 is 'increasing and

I2 is 'increasing ; :: thesis: ( P1 = P2 & I1 = I2 )

dom I1 = {} by A2, A4, A6, RELAT_1:27;

then A7: I1 = {} ;

rng P1 = {} by A2, A4, A6, RELAT_1:28, RELAT_1:38;

then P1 = {} ;

hence ( P1 = P2 & I1 = I2 ) by A3, A5, A7; :: thesis: verum

end;for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let F be Function of Ne,Ke; :: thesis: ( F = {} implies for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 ) )

assume A2: F = {} ; :: thesis: for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let I1, I2 be Function of Ne,Me; :: thesis: for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let P1, P2 be Function; :: thesis: ( P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing implies ( P1 = P2 & I1 = I2 ) )

assume that

P1 is one-to-one and

P2 is one-to-one and

A3: rng I1 = rng I2 and

A4: rng I1 = dom P1 and

A5: dom P1 = dom P2 and

A6: F = P1 * I1 and

F = P2 * I2 and

I1 is 'increasing and

I2 is 'increasing ; :: thesis: ( P1 = P2 & I1 = I2 )

dom I1 = {} by A2, A4, A6, RELAT_1:27;

then A7: I1 = {} ;

rng P1 = {} by A2, A4, A6, RELAT_1:28, RELAT_1:38;

then P1 = {} ;

hence ( P1 = P2 & I1 = I2 ) by A3, A5, A7; :: thesis: verum

S

S

proof

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

_{2}[F9]
; :: thesis: verum

end;S

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

S

now :: thesis: S_{2}[F9]end;

hence
Sper cases
( F9 = {} or F9 <> {} )
;

end;

suppose A10:
F9 <> {}
; :: thesis: for Ne, Ke, Me being Subset of NAT

for F being Function of Ne,Ke st F = F9 holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

for F being Function of Ne,Ke st F = F9 holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let Ne, Ke, Me be Subset of NAT; :: thesis: for F being Function of Ne,Ke st F = F9 holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let F be Function of Ne,Ke; :: thesis: ( F = F9 implies for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 ) )

assume A11: F = F9 ; :: thesis: for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

not Ke is empty by A10, A11;

then reconsider domF = dom F as non empty Subset of NAT by A10, A11, FUNCT_2:def 1;

set m = min* (dom F);

let I1, I2 be Function of Ne,Me; :: thesis: for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let P1, P2 be Function; :: thesis: ( P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing implies ( P1 = P2 & I1 = I2 ) )

assume that

A12: P1 is one-to-one and

A13: P2 is one-to-one and

A14: rng I1 = rng I2 and

A15: rng I1 = dom P1 and

A16: dom P1 = dom P2 and

A17: F = P1 * I1 and

A18: F = P2 * I2 and

A19: I1 is 'increasing and

A20: I2 is 'increasing ; :: thesis: ( P1 = P2 & I1 = I2 )

dom I1 = dom F by A15, A17, RELAT_1:27;

then A21: min* (rng I1) = I1 . (min* (dom F)) by A19, Th62;

reconsider I = (rng I1) \ {(I1 . (min* (dom F)))} as Subset of NAT by XBOOLE_1:1;

reconsider D = (dom F) \ (F " {(F . (min* (dom F)))}) as Subset of NAT by XBOOLE_1:1;

A22: for I being Function of Ne,Me

for P being Function st P is one-to-one & rng I = dom P & F = P * I & I is 'increasing holds

( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) )

dom I2 = dom F by A14, A15, A16, A18, RELAT_1:27;

then A52: min* (rng I2) = I2 . (min* (dom F)) by A20, Th62;

then A53: P2 | I is one-to-one by A13, A14, A15, A16, A18, A20, A22, A21;

A54: dom (I2 | D) = D by A13, A14, A15, A16, A18, A20, A22;

A55: dom (I1 | D) = D by A12, A15, A17, A19, A22;

A56: rng (I1 | D) = I by A12, A15, A17, A19, A22;

rng (I2 | D) = I by A13, A14, A15, A16, A18, A20, A22, A21, A52;

then reconsider I1D = I1 | D, I2D = I2 | D as Function of D,I by A55, A54, A56, FUNCT_2:1;

A57: I2D is 'increasing by A13, A14, A15, A16, A18, A20, A22, A21, A52;

A58: rng I1D = I by A12, A15, A17, A19, A22;

then A59: rng I1D = dom (P1 | I) by A12, A15, A17, A19, A22;

reconsider rFD = rng (F | D) as Subset of NAT by XBOOLE_1:1;

(dom F) /\ D = D by XBOOLE_1:28, XBOOLE_1:36;

then dom (F | D) = D by RELAT_1:61;

then reconsider FD = F | D as Function of D,rFD by FUNCT_2:1;

A60: FD = (P1 | I) * I1D by A12, A15, A17, A19, A22;

A61: FD = (P2 | I) * I2D by A13, A14, A15, A16, A18, A20, A22, A21, A52;

min* (dom F) in domF by NAT_1:def 1;

then A62: F . (min* (dom F)) in rng F by FUNCT_1:def 3;

dom (P1 | I) = I by A12, A15, A17, A19, A22;

then A63: dom (P1 | I) = dom (P2 | I) by A13, A14, A15, A16, A18, A20, A22, A21, A52;

A64: I1D is 'increasing by A12, A15, A17, A19, A22;

A65: rng I1D = rng I2D by A13, A14, A15, A16, A18, A20, A22, A21, A52, A58;

for x being object st x in dom P1 holds

P1 . x = P2 . x

I2 is Function of (dom I2),(rng I2) by FUNCT_2:1;

then A75: I2 = (id (rng I2)) * I2 by FUNCT_2:17;

I1 is Function of (dom I1),(rng I1) by FUNCT_2:1;

then A76: I1 = (id (rng I1)) * I1 by FUNCT_2:17;

(P1 ") * P1 = id (dom P1) by A12, FUNCT_1:39;

then A77: I1 = (P1 ") * (P1 * I1) by A15, A76, RELAT_1:36;

(P2 ") * P2 = id (dom P2) by A13, FUNCT_1:39;

hence ( P1 = P2 & I1 = I2 ) by A14, A15, A17, A18, A74, A75, A77, RELAT_1:36; :: thesis: verum

end;for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let F be Function of Ne,Ke; :: thesis: ( F = F9 implies for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 ) )

assume A11: F = F9 ; :: thesis: for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

not Ke is empty by A10, A11;

then reconsider domF = dom F as non empty Subset of NAT by A10, A11, FUNCT_2:def 1;

set m = min* (dom F);

let I1, I2 be Function of Ne,Me; :: thesis: for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 )

let P1, P2 be Function; :: thesis: ( P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing implies ( P1 = P2 & I1 = I2 ) )

assume that

A12: P1 is one-to-one and

A13: P2 is one-to-one and

A14: rng I1 = rng I2 and

A15: rng I1 = dom P1 and

A16: dom P1 = dom P2 and

A17: F = P1 * I1 and

A18: F = P2 * I2 and

A19: I1 is 'increasing and

A20: I2 is 'increasing ; :: thesis: ( P1 = P2 & I1 = I2 )

dom I1 = dom F by A15, A17, RELAT_1:27;

then A21: min* (rng I1) = I1 . (min* (dom F)) by A19, Th62;

reconsider I = (rng I1) \ {(I1 . (min* (dom F)))} as Subset of NAT by XBOOLE_1:1;

reconsider D = (dom F) \ (F " {(F . (min* (dom F)))}) as Subset of NAT by XBOOLE_1:1;

A22: for I being Function of Ne,Me

for P being Function st P is one-to-one & rng I = dom P & F = P * I & I is 'increasing holds

( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) )

proof

then A51:
P1 | I is one-to-one
by A12, A15, A17, A19;
A23:
F . (min* (dom F)) in {(F . (min* (dom F)))}
by TARSKI:def 1;

let I be Function of Ne,Me; :: thesis: for P being Function st P is one-to-one & rng I = dom P & F = P * I & I is 'increasing holds

( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) )

let P be Function; :: thesis: ( P is one-to-one & rng I = dom P & F = P * I & I is 'increasing implies ( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) ) )

assume that

A24: P is one-to-one and

A25: rng I = dom P and

A26: F = P * I and

A27: I is 'increasing ; :: thesis: ( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) )

A28: (dom P) /\ ((rng I) \ {(I . (min* (dom F)))}) = (rng I) \ {(I . (min* (dom F)))} by A25, XBOOLE_1:28, XBOOLE_1:36;

min* (dom F) in domF by NAT_1:def 1;

then F . (min* (dom F)) in rng F by FUNCT_1:def 3;

then consider x being set such that

x in dom P and

x in rng I and

P " {(F . (min* (dom F)))} = {x} and

A29: I " {x} = F " {(F . (min* (dom F)))} by A24, A26, Th61;

A30: dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (dom P) /\ ((rng I) \ {(I . (min* (dom F)))}) by RELAT_1:61;

A31: dom F = dom I by A25, A26, RELAT_1:27;

then A32: (dom I) /\ D = D by XBOOLE_1:28, XBOOLE_1:36;

min* (dom F) in domF by NAT_1:def 1;

then min* (dom F) in I " {x} by A29, A23, FUNCT_1:def 7;

then I . (min* (dom F)) in {x} by FUNCT_1:def 7;

then A33: I . (min* (dom F)) = x by TARSKI:def 1;

A34: for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing

A43: dom (I | D) = (dom I) /\ D by RELAT_1:61;

A44: rng (I | D) = (rng I) \ {(I . (min* (dom F)))} by A29, A33, A31, Th54;

A45: for x being object st x in dom (F | D) holds

(F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x)

then dom (F | D) = D by RELAT_1:61;

then for x being object holds

( x in dom (F | D) iff ( x in dom (I | D) & (I | D) . x in dom (P | ((rng I) \ {(I . (min* (dom F)))})) ) ) by A43, A32, A30, A28, A44, FUNCT_1:def 3;

hence ( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) ) by A24, A29, A33, A31, A32, A28, A45, A34, Th54, FUNCT_1:10, FUNCT_1:52, RELAT_1:61; :: thesis: verum

end;let I be Function of Ne,Me; :: thesis: for P being Function st P is one-to-one & rng I = dom P & F = P * I & I is 'increasing holds

( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) )

let P be Function; :: thesis: ( P is one-to-one & rng I = dom P & F = P * I & I is 'increasing implies ( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) ) )

assume that

A24: P is one-to-one and

A25: rng I = dom P and

A26: F = P * I and

A27: I is 'increasing ; :: thesis: ( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) )

A28: (dom P) /\ ((rng I) \ {(I . (min* (dom F)))}) = (rng I) \ {(I . (min* (dom F)))} by A25, XBOOLE_1:28, XBOOLE_1:36;

min* (dom F) in domF by NAT_1:def 1;

then F . (min* (dom F)) in rng F by FUNCT_1:def 3;

then consider x being set such that

x in dom P and

x in rng I and

P " {(F . (min* (dom F)))} = {x} and

A29: I " {x} = F " {(F . (min* (dom F)))} by A24, A26, Th61;

A30: dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (dom P) /\ ((rng I) \ {(I . (min* (dom F)))}) by RELAT_1:61;

A31: dom F = dom I by A25, A26, RELAT_1:27;

then A32: (dom I) /\ D = D by XBOOLE_1:28, XBOOLE_1:36;

min* (dom F) in domF by NAT_1:def 1;

then min* (dom F) in I " {x} by A29, A23, FUNCT_1:def 7;

then I . (min* (dom F)) in {x} by FUNCT_1:def 7;

then A33: I . (min* (dom F)) = x by TARSKI:def 1;

A34: for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing

proof

set rI = (rng I) \ {(I . (min* (dom F)))};
let M be Subset of NAT; :: thesis: ( M = (rng I) \ {(I . (min* (dom F)))} implies for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing )

assume M = (rng I) \ {(I . (min* (dom F)))} ; :: thesis: for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing

let I1 be Function of D,M; :: thesis: ( I1 = I | D implies I1 is 'increasing )

assume A35: I1 = I | D ; :: thesis: I1 is 'increasing

A36: rng I1 = (rng I) \ {(I . (min* (dom F)))} by A29, A33, A31, A35, Th54;

let l be Nat; :: according to STIRL2_1:def 3 :: thesis: for m being Nat st l in rng I1 & m in rng I1 & l < m holds

min* (I1 " {l}) < min* (I1 " {m})

let n be Nat; :: thesis: ( l in rng I1 & n in rng I1 & l < n implies min* (I1 " {l}) < min* (I1 " {n}) )

assume that

A37: l in rng I1 and

A38: n in rng I1 and

A39: l < n ; :: thesis: min* (I1 " {l}) < min* (I1 " {n})

A40: n in rng I by A38, A36, ZFMISC_1:56;

n <> I . (min* (dom F)) by A38, A36, ZFMISC_1:56;

then A41: I1 " {n} = I " {n} by A29, A33, A31, A35, Th54;

l <> I . (min* (dom F)) by A37, A36, ZFMISC_1:56;

then A42: I1 " {l} = I " {l} by A29, A33, A31, A35, Th54;

l in rng I by A37, A36, ZFMISC_1:56;

hence min* (I1 " {l}) < min* (I1 " {n}) by A27, A39, A40, A42, A41; :: thesis: verum

end;I1 is 'increasing )

assume M = (rng I) \ {(I . (min* (dom F)))} ; :: thesis: for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing

let I1 be Function of D,M; :: thesis: ( I1 = I | D implies I1 is 'increasing )

assume A35: I1 = I | D ; :: thesis: I1 is 'increasing

A36: rng I1 = (rng I) \ {(I . (min* (dom F)))} by A29, A33, A31, A35, Th54;

let l be Nat; :: according to STIRL2_1:def 3 :: thesis: for m being Nat st l in rng I1 & m in rng I1 & l < m holds

min* (I1 " {l}) < min* (I1 " {m})

let n be Nat; :: thesis: ( l in rng I1 & n in rng I1 & l < n implies min* (I1 " {l}) < min* (I1 " {n}) )

assume that

A37: l in rng I1 and

A38: n in rng I1 and

A39: l < n ; :: thesis: min* (I1 " {l}) < min* (I1 " {n})

A40: n in rng I by A38, A36, ZFMISC_1:56;

n <> I . (min* (dom F)) by A38, A36, ZFMISC_1:56;

then A41: I1 " {n} = I " {n} by A29, A33, A31, A35, Th54;

l <> I . (min* (dom F)) by A37, A36, ZFMISC_1:56;

then A42: I1 " {l} = I " {l} by A29, A33, A31, A35, Th54;

l in rng I by A37, A36, ZFMISC_1:56;

hence min* (I1 " {l}) < min* (I1 " {n}) by A27, A39, A40, A42, A41; :: thesis: verum

A43: dom (I | D) = (dom I) /\ D by RELAT_1:61;

A44: rng (I | D) = (rng I) \ {(I . (min* (dom F)))} by A29, A33, A31, Th54;

A45: for x being object st x in dom (F | D) holds

(F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x)

proof

(dom F) /\ D = D
by XBOOLE_1:28, XBOOLE_1:36;
let x be object ; :: thesis: ( x in dom (F | D) implies (F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x) )

assume A46: x in dom (F | D) ; :: thesis: (F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x)

A47: x in (dom F) /\ D by A46, RELAT_1:61;

then A48: x in dom F by XBOOLE_0:def 4;

(I | D) . x in dom (P | ((rng I) \ {(I . (min* (dom F)))})) by A31, A43, A30, A28, A44, A47, FUNCT_1:def 3;

then A49: (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x) = P . ((I | D) . x) by FUNCT_1:47;

A50: (F | D) . x = F . x by A46, FUNCT_1:47;

I . x = (I | D) . x by A31, A43, A47, FUNCT_1:47;

hence (F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x) by A26, A48, A49, A50, FUNCT_1:12; :: thesis: verum

end;assume A46: x in dom (F | D) ; :: thesis: (F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x)

A47: x in (dom F) /\ D by A46, RELAT_1:61;

then A48: x in dom F by XBOOLE_0:def 4;

(I | D) . x in dom (P | ((rng I) \ {(I . (min* (dom F)))})) by A31, A43, A30, A28, A44, A47, FUNCT_1:def 3;

then A49: (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x) = P . ((I | D) . x) by FUNCT_1:47;

A50: (F | D) . x = F . x by A46, FUNCT_1:47;

I . x = (I | D) . x by A31, A43, A47, FUNCT_1:47;

hence (F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x) by A26, A48, A49, A50, FUNCT_1:12; :: thesis: verum

then dom (F | D) = D by RELAT_1:61;

then for x being object holds

( x in dom (F | D) iff ( x in dom (I | D) & (I | D) . x in dom (P | ((rng I) \ {(I . (min* (dom F)))})) ) ) by A43, A32, A30, A28, A44, FUNCT_1:def 3;

hence ( dom (I | D) = D & rng (I | D) = (rng I) \ {(I . (min* (dom F)))} & dom (P | ((rng I) \ {(I . (min* (dom F)))})) = (rng I) \ {(I . (min* (dom F)))} & F | D = (P | ((rng I) \ {(I . (min* (dom F)))})) * (I | D) & P | ((rng I) \ {(I . (min* (dom F)))}) is one-to-one & ( for M being Subset of NAT st M = (rng I) \ {(I . (min* (dom F)))} holds

for I1 being Function of D,M st I1 = I | D holds

I1 is 'increasing ) ) by A24, A29, A33, A31, A32, A28, A45, A34, Th54, FUNCT_1:10, FUNCT_1:52, RELAT_1:61; :: thesis: verum

dom I2 = dom F by A14, A15, A16, A18, RELAT_1:27;

then A52: min* (rng I2) = I2 . (min* (dom F)) by A20, Th62;

then A53: P2 | I is one-to-one by A13, A14, A15, A16, A18, A20, A22, A21;

A54: dom (I2 | D) = D by A13, A14, A15, A16, A18, A20, A22;

A55: dom (I1 | D) = D by A12, A15, A17, A19, A22;

A56: rng (I1 | D) = I by A12, A15, A17, A19, A22;

rng (I2 | D) = I by A13, A14, A15, A16, A18, A20, A22, A21, A52;

then reconsider I1D = I1 | D, I2D = I2 | D as Function of D,I by A55, A54, A56, FUNCT_2:1;

A57: I2D is 'increasing by A13, A14, A15, A16, A18, A20, A22, A21, A52;

A58: rng I1D = I by A12, A15, A17, A19, A22;

then A59: rng I1D = dom (P1 | I) by A12, A15, A17, A19, A22;

reconsider rFD = rng (F | D) as Subset of NAT by XBOOLE_1:1;

(dom F) /\ D = D by XBOOLE_1:28, XBOOLE_1:36;

then dom (F | D) = D by RELAT_1:61;

then reconsider FD = F | D as Function of D,rFD by FUNCT_2:1;

A60: FD = (P1 | I) * I1D by A12, A15, A17, A19, A22;

A61: FD = (P2 | I) * I2D by A13, A14, A15, A16, A18, A20, A22, A21, A52;

min* (dom F) in domF by NAT_1:def 1;

then A62: F . (min* (dom F)) in rng F by FUNCT_1:def 3;

dom (P1 | I) = I by A12, A15, A17, A19, A22;

then A63: dom (P1 | I) = dom (P2 | I) by A13, A14, A15, A16, A18, A20, A22, A21, A52;

A64: I1D is 'increasing by A12, A15, A17, A19, A22;

A65: rng I1D = rng I2D by A13, A14, A15, A16, A18, A20, A22, A21, A52, A58;

for x being object st x in dom P1 holds

P1 . x = P2 . x

proof

then A74:
P1 = P2
by A16;
A66:
min* (dom F) in domF
by NAT_1:def 1;

dom I1 = dom F by A15, A17, RELAT_1:27;

then I1 . (min* (dom F)) in rng I1 by A66, FUNCT_1:def 3;

then A67: dom P1 = I \/ {(I1 . (min* (dom F)))} by A15, ZFMISC_1:116;

let x be object ; :: thesis: ( x in dom P1 implies P1 . x = P2 . x )

assume A68: x in dom P1 ; :: thesis: P1 . x = P2 . x

end;dom I1 = dom F by A15, A17, RELAT_1:27;

then I1 . (min* (dom F)) in rng I1 by A66, FUNCT_1:def 3;

then A67: dom P1 = I \/ {(I1 . (min* (dom F)))} by A15, ZFMISC_1:116;

let x be object ; :: thesis: ( x in dom P1 implies P1 . x = P2 . x )

assume A68: x in dom P1 ; :: thesis: P1 . x = P2 . x

now :: thesis: P1 . x = P2 . xend;

hence
P1 . x = P2 . x
; :: thesis: verumper cases
( x in I or x in {(I1 . (min* (dom F)))} )
by A68, A67, XBOOLE_0:def 3;

end;

suppose A69:
x in I
; :: thesis: P1 . x = P2 . x

(dom P1) /\ I = I
by A15, XBOOLE_1:28, XBOOLE_1:36;

then x in dom (P1 | I) by A69, RELAT_1:61;

then A70: (P1 | I) . x = P1 . x by FUNCT_1:47;

(dom P2) /\ I = I by A15, A16, XBOOLE_1:28, XBOOLE_1:36;

then x in dom (P2 | I) by A69, RELAT_1:61;

then (P2 | I) . x = P2 . x by FUNCT_1:47;

hence P1 . x = P2 . x by A9, A11, A62, A51, A53, A65, A59, A63, A60, A61, A64, A57, A70; :: thesis: verum

end;then x in dom (P1 | I) by A69, RELAT_1:61;

then A70: (P1 | I) . x = P1 . x by FUNCT_1:47;

(dom P2) /\ I = I by A15, A16, XBOOLE_1:28, XBOOLE_1:36;

then x in dom (P2 | I) by A69, RELAT_1:61;

then (P2 | I) . x = P2 . x by FUNCT_1:47;

hence P1 . x = P2 . x by A9, A11, A62, A51, A53, A65, A59, A63, A60, A61, A64, A57, A70; :: thesis: verum

suppose A71:
x in {(I1 . (min* (dom F)))}
; :: thesis: P1 . x = P2 . x

A72:
min* (dom F) in domF
by NAT_1:def 1;

A73: x = I1 . (min* (dom F)) by A71, TARSKI:def 1;

then F . (min* (dom F)) = P1 . x by A17, A72, FUNCT_1:12;

hence P1 . x = P2 . x by A14, A18, A21, A52, A73, A72, FUNCT_1:12; :: thesis: verum

end;A73: x = I1 . (min* (dom F)) by A71, TARSKI:def 1;

then F . (min* (dom F)) = P1 . x by A17, A72, FUNCT_1:12;

hence P1 . x = P2 . x by A14, A18, A21, A52, A73, A72, FUNCT_1:12; :: thesis: verum

I2 is Function of (dom I2),(rng I2) by FUNCT_2:1;

then A75: I2 = (id (rng I2)) * I2 by FUNCT_2:17;

I1 is Function of (dom I1),(rng I1) by FUNCT_2:1;

then A76: I1 = (id (rng I1)) * I1 by FUNCT_2:17;

(P1 ") * P1 = id (dom P1) by A12, FUNCT_1:39;

then A77: I1 = (P1 ") * (P1 * I1) by A15, A76, RELAT_1:36;

(P2 ") * P2 = id (dom P2) by A13, FUNCT_1:39;

hence ( P1 = P2 & I1 = I2 ) by A14, A15, A17, A18, A74, A75, A77, RELAT_1:36; :: thesis: verum

S

hence for F being Function of Ne,Ke st rng F is finite holds

for I1, I2 being Function of Ne,Me

for P1, P2 being Function st P1 is one-to-one & P2 is one-to-one & rng I1 = rng I2 & rng I1 = dom P1 & dom P1 = dom P2 & F = P1 * I1 & F = P2 * I2 & I1 is 'increasing & I2 is 'increasing holds

( P1 = P2 & I1 = I2 ) ; :: thesis: verum