theorem :: FINSEQ_4:64

for A, B being finite set
for f being Function of A,B st card A = card B & rng f = B holds
f is one-to-one by Lm1;