:: deftheorem defines Radical MOEBIUS1:def 7 :
for n being non zero Nat holds Radical n = Product (PFactors n);