rng (Sgm (PrimeDivisors 1)) = PrimeDivisors 1 by FINSEQ_1:def 14;
hence PrimeDivisorsFS 1 is empty by NUMBER12:51; :: thesis: verum