theorem Th40: :: STIRL2_1:40

for k, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm (k + 1)) st f is onto & f is "increasing & f = g | (Segm n) & g . n = k holds
( g is onto & g is "increasing & g " {(g . n)} = {n} )