theorem Th39: :: STIRL2_1:39

for k, m, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm (k + m)) st f is onto & f is "increasing & f = g | n holds
for i, j being Nat st i in rng g & j in rng g & i < j holds
min* (g " {i}) < min* (g " {j})