let n, k be Nat; :: thesis: card { f where f is Function of n,k : ( f is onto & f is "increasing ) } is Element of NAT
set F = { f where f is Function of n,k : ( f is onto & f is "increasing ) } ;
consider m being Nat such that
A1: { f where f is Function of n,k : ( f is onto & f is "increasing ) } ,m are_equipotent by Th24, CARD_1:74;
( card { f where f is Function of n,k : ( f is onto & f is "increasing ) } = card m & card m = m ) by A1, CARD_1:21, CARD_1:def 5;
hence card { f where f is Function of n,k : ( f is onto & f is "increasing ) } is Element of NAT ; :: thesis: verum