:: deftheorem defines canFS FINSEQ_1:def 19 :
for A being finite set holds canFS A = the one-to-one onto FinSequence of A;