theorem Th25: :: STIRL2_1:25

for n, k being Nat holds card { f where f is Function of (Segm n),(Segm k) : ( f is onto & f is "increasing ) } is Element of NAT