rng (Sgm (PrimeDivisors n)) = PrimeDivisors n by FINSEQ_1:def 14;
hence Sgm (PrimeDivisors n) is FinSequence of SetPrimes by NUMBER12:45, FINSEQ_1:def 4; :: thesis: verum