theorem Th37: :: STIRL2_1:37

for k, n being Nat
for f being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f " {(f . n)} = {n} holds
( rng (f | n) c= Segm k & ( for g being Function of (Segm n),(Segm k) st g = f | n holds
( g is onto & g is "increasing ) ) )