theorem :: LEXBFS:1

for A, B being Element of NAT
for X being non empty set
for F being sequence of X st F is one-to-one holds
card { (F . w) where w is Element of NAT : ( A <= w & w <= A + B ) } = B + 1