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