theorem :: STIRL2_1:21

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