let n, k be Nat; :: thesis: { f where f is Function of n,k : ( f is onto & f is "increasing ) } is finite
defpred S₁[ Function of n,k] means ( $1 is onto & $1 is "increasing );
{ f where f is Function of n,k : S₁[f] } is finite from STIRL2_1:sch 1();
hence { f where f is Function of n,k : ( f is onto & f is "increasing ) } is finite ; :: thesis: verum