let n be non zero Nat; :: thesis: ( PrimeDivisorsFS n is empty implies n = 1 )
rng (PrimeDivisorsFS n) = PrimeDivisors n by FINSEQ_1:def 14;
hence ( PrimeDivisorsFS n is empty implies n = 1 ) by Th49; :: thesis: verum