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

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