for m being Element of NAT
for X being finite set st card X = m holds
ex fp being FinSequence st
( len fp = m & ( for a being Element of NAT st a in dom fp holds
fp . a in X ) & fp is one-to-one )