let p be Prime; :: thesis: for n being non zero Nat holds
( p divides n iff p divides Radical n )
let n be non zero Nat; :: 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: p in support (PFactors n) by Def6;
then p in rng (canFS (support (PFactors n))) by FUNCT_2:def 3;
then consider y being object such that
A5: y in dom (canFS (support (PFactors n))) and
A6: p = (canFS (support (PFactors n))) . y by FUNCT_1:def 3;
consider f being FinSequence of COMPLEX such that
A7: Product (PFactors n) = Product f and
A8: f = (PFactors n) * (canFS (support (PFactors n))) by NAT_3:def 5;
( rng (PFactors n) c= NAT & rng f c= rng (PFactors n) ) by A8, RELAT_1:26, VALUED_0:def 6;
then A9: rng f c= NAT ;
support (PFactors n) c= dom (PFactors n) by PRE_POLY:37;
then A10: y in dom f by A4, A8, A5, A6, FUNCT_1:11;
reconsider f = f as FinSequence of NAT by A9, FINSEQ_1:def 4;
(PFactors n) . p = p by A3, Def6;
then f . y = p by A8, A6, A10, FUNCT_1:12;
then p in rng f by A10, FUNCT_1:3;
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