let A be finite set ; :: thesis: dom (canFS A) = Seg (card A)
len (canFS A) = card A by FINSEQ_1:93;
hence dom (canFS A) = Seg (card A) by FINSEQ_1:def 3; :: thesis: verum