let n, k be Nat; :: thesis: card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is Element of NAT
set F = { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } ;
{ f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is finite by Th24;
then reconsider m = card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } as Nat ;
card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } = card m ;
hence card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is Element of NAT ; :: thesis: verum