theorem Th41: :: STIRL2_1:41

for k, n being Nat
for f being Function of (Segm n),(Segm k)
for g being Function of (Segm (n + 1)),(Segm k) 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} )