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 S1[ set , Function] means \$1 = \$2 . (min* (dom \$2));
defpred S2[ 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: S2[ {} ]
proof
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 ;
then A7: I1 = {} ;
rng P1 = {} by ;
then P1 = {} ;
hence ( P1 = P2 & I1 = I2 ) by A3, A5, A7; :: thesis: verum
end;
A8: 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 A9: for x being set st x in rng F9 & S1[x,F9] holds
S2[F9 | ((dom F9) \ (F9 " {x}))] ; :: thesis: S2[F9]
now :: thesis: S2[F9]
per cases ( F9 = {} or F9 <> {} ) ;
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 )

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 ;
then reconsider domF = dom F as non empty Subset of NAT by ;
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 ;
then A21: min* (rng I1) = I1 . (min* (dom F)) by ;
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: 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 ;
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 ;
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 ;
then A32: (dom I) /\ D = D by ;
min* (dom F) in domF by NAT_1:def 1;
then min* (dom F) in I " {x} by ;
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: ( 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 ;
n <> I . (min* (dom F)) by ;
then A41: I1 " {n} = I " {n} by A29, A33, A31, A35, Th54;
l <> I . (min* (dom F)) by ;
then A42: I1 " {l} = I " {l} by A29, A33, A31, A35, Th54;
l in rng I by ;
hence min* (I1 " {l}) < min* (I1 " {n}) by A27, A39, A40, A42, A41; :: thesis: verum
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 ;
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: ( 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 ;
then A48: x in dom F by XBOOLE_0:def 4;
(I | D) . x in dom (P | ((rng I) \ {(I . (min* (dom F)))})) by ;
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 ;
I . x = (I | D) . x by ;
hence (F | D) . x = (P | ((rng I) \ {(I . (min* (dom F)))})) . ((I | D) . x) by ; :: thesis: verum
end;
(dom F) /\ D = D by ;
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 ;
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 ; :: thesis: verum
end;
then A51: P1 | I is one-to-one by A12, A15, A17, A19;
dom I2 = dom F by ;
then A52: min* (rng I2) = I2 . (min* (dom F)) by ;
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 ;
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 ;
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 ;
then I1 . (min* (dom F)) in rng I1 by ;
then A67: dom P1 = I \/ {(I1 . (min* (dom F)))} by ;
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 . x
per cases ( x in I or x in {(I1 . (min* (dom F)))} ) by ;
suppose A69: x in I ; :: thesis: P1 . x = P2 . x
(dom P1) /\ I = I by ;
then x in dom (P1 | I) by ;
then A70: (P1 | I) . x = P1 . x by FUNCT_1:47;
(dom P2) /\ I = I by ;
then x in dom (P2 | I) by ;
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;
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 ;
then F . (min* (dom F)) = P1 . x by ;
hence P1 . x = P2 . x by ; :: thesis: verum
end;
end;
end;
hence P1 . x = P2 . x ; :: thesis: verum
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 ;
then A77: I1 = (P1 ") * (P1 * I1) by ;
(P2 ") * P2 = id (dom P2) by ;
hence ( P1 = P2 & I1 = I2 ) by ; :: thesis: verum
end;
end;
end;
hence S2[F9] ; :: thesis: verum
end;
for F being Function st rng F is finite holds
S2[F] from 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