theorem Th15: :: STIRL2_1:15

for k, n being Nat
for f being Function of (Segm n),(Segm k) st n = 0 & k = 0 holds
( f is onto & f is "increasing )