theorem Th43: :: STIRL2_1:43

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