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