theorem Th20: :: STIRL2_1:20

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto & f is "increasing & n = k holds
f = id n