theorem :: FINSEQ_1:95

for A being finite set holds (canFS A) " is Function of A,(Seg (card A))