let Ke, Ne, Me be Subset of NAT; :: thesis:
defpred S₁[ set , Function] means $1 = $2 . (min* (dom $2));
defpred S₂[ 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₂[ {} ]

let Ne, Ke, Me be Subset of NAT; :: thesis:
let F be Function of Ne,Ke; :: thesis:
assume A2: F = {} ; :: thesis:
let I1, I2 be Function of Ne,Me; :: thesis:
let P1, P2 be Function; :: thesis:
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:
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:

end;

A8: for F being Function st ( for x being set st x in rng F & S₁[x,F] holds
S₂[F | ((dom F) \ (F " {x}))] ) holds
S₂[F]

proof

let F9 be Function; :: thesis:
assume A9: for x being set st x in rng F9 & S₁[x,F9] holds
S₂[F9 | ((dom F9) \ (F9 " {x}))] ; :: thesis:

now :: thesis:

per cases ;

suppose F9 = {} ; :: thesis:

hence S₂[F9] by A1; :: thesis:

end;

suppose A10: F9 <> {} ; :: thesis:

let Ne, Ke, Me be Subset of NAT; :: thesis:
let F be Function of Ne,Ke; :: thesis:
assume A11: F = F9 ; :: thesis:
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:
let P1, P2 be Function; :: thesis:
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:
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

A23: F . (min* (dom F)) in {(F . (min* (dom F)))} by TARSKI:def 1;
let I be Function of Ne,Me; :: thesis:
let P be Function; :: thesis:
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:
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

let M be Subset of NAT; :: thesis:
assume M = (rng I) \ {(I . (min* (dom F)))} ; :: thesis:
let I1 be Function of D,M; :: thesis:
assume A35: I1 = I | D ; :: thesis:
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:
let n be Nat; :: thesis:
assume that
A37: l in rng I1 and
A38: n in rng I1 and
A39: l < n ; :: thesis:
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:

end;

set rI = (rng I) \ {(I . (min* (dom F)))};
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

let x be object ; :: thesis:
assume A46: x in dom (F | D) ; :: thesis:
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:

end;

(dom F) /\ D = D by XBOOLE_1:28, XBOOLE_1:36;
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:

end;

then A51: P1 | I is one-to-one by A12, A15, A17, A19;
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

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:
assume A68: x in dom P1 ; :: thesis:

now :: thesis:

per cases by A68, A67, XBOOLE_0:def 3;

suppose A69: x in I ; :: thesis:

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

end;

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

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:

end;

hence P1 . x = P2 . x ; :: thesis:

end;

then A74: P1 = P2 by A16;
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:

end;

hence S₂[F9] ; :: thesis:

end;

for F being Function st rng F is finite holds
S₂[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: