theorem Th34: :: STIRL2_1:34

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
f . n = k