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_{1}[ Function of (Segm n),(Segm k)] means ( $1 is onto & $1 is "increasing );

{ f where f is Function of (Segm n),(Segm k) : S_{1}[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

defpred S

{ f where f is Function of (Segm n),(Segm k) : S

hence { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is finite ; :: thesis: verum