theorem :: FINSEQ_4:63

for A, B being finite set
for f being Function of A,B st card A = card B holds
( f is one-to-one iff f is onto ) by Lemacik, Lm1;