for Ke, Ne, Me being Subset of NAT
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 )