theorem Th16: :: STIRL2_1:16

for k, m, n being Nat
for f being Function of (Segm n),(Segm k) st n > 0 holds
min* (f " {m}) <= n - 1