theorem Th47: :: NUMBER14:47
for n being non zero Nat
for i being Nat st i in dom (PrimeDivisorsFS n) holds
(PrimeDivisorsFS n) . i is prime