theorem Th45: :: STIRL2_1:45

for k, n being Nat holds k * (n block k) = card { f where f is Function of (Segm (n + 1)),(Segm k) : ( f is onto & f is "increasing & f " {(f . n)} <> {n} ) }