theorem Th17: :: STIRL2_1:17

for k, n being Nat
for f being Function of (Segm n),(Segm k) st f is onto holds
n >= k