let p be Prime; :: thesis: for n being non zero natural number holds
( p divides n iff p divides Radical n )
let n be non zero natural number ; :: thesis: ( p divides n iff p divides Radical n )
thus ( p divides n implies p divides Radical n ) :: thesis: ( p divides Radical n implies p divides n )

proof

assume that
A1: p divides n and
A2: not p divides Radical n ; :: thesis: contradiction
A3: p in support (pfexp n) by A1, NAT_3:37;
then A4: (PFactors n) . p = p by Def6;
A5: p in support (PFactors n) by A3, Def6;
A6: support (PFactors n) c= dom (PFactors n) by POLYNOM1:41;
consider f being FinSequence of COMPLEX such that
A7: ( Product (PFactors n) = Product f & f = (PFactors n) * (canFS (support (PFactors n))) ) by NAT_3:def 5;
p in rng (canFS (support (PFactors n))) by A5, FUNCT_2:def 3;
then consider y being set such that
A8: ( y in dom (canFS (support (PFactors n))) & p = (canFS (support (PFactors n))) . y ) by FUNCT_1:def 5;
A9: y in dom f by A5, A6, A7, A8, FUNCT_1:21;
A10: rng (PFactors n) c= NAT by VALUED_0:def 6;
rng f c= rng (PFactors n) by A7, RELAT_1:45;
then rng f c= NAT by A10, XBOOLE_1:1;
then reconsider f = f as FinSequence of NAT by FINSEQ_1:def 4;
f . y = p by A4, A7, A8, A9, FUNCT_1:22;
then p in rng f by A9, FUNCT_1:12;
hence contradiction by A2, A7, NAT_3:7; :: thesis: verum

end;

assume A11: p divides Radical n ; :: thesis: p divides n
Radical n divides n by Th55;
hence p divides n by A11, NAT_D:4; :: thesis: verum