for m, n being non zero Element of NAT st m,n are_coprime holds
PFactors (m * n) = (PFactors m) + (PFactors n)