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