theorem Th38: :: STIRL2_1:38

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