let p be Prime; :: thesis: dom (canFS (Seg p)) = Seg p
len (canFS (Seg p)) = card (Seg p) by FINSEQ_1:93
.= p by FINSEQ_1:57 ;
hence dom (canFS (Seg p)) = Seg p by FINSEQ_1:def 3; :: thesis: verum