theorem Th36: :: STIRL2_1:36

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