let k, n be Nat; :: thesis: ( n < k implies n block k = 0 )
set F = { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ;
assume A1: n < k ; :: thesis: n block k = 0
{ f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } = {}

proof

assume { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } <> {} ; :: thesis: contradiction
then consider x being object such that
A2: x in { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } by XBOOLE_0:def 1;
ex f being Function of (Segm n),(Segm k) st
( x = f & f is onto & f is "increasing ) by A2;
hence contradiction by A1, Th17; :: thesis: verum

end;

hence n block k = 0 ; :: thesis: verum