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
A3: p in support () by ;
then A4: p in support () by Def6;
then p in rng (canFS (support ())) by FUNCT_2:def 3;
then consider y being object such that
A5: y in dom (canFS (support ())) and
A6: p = (canFS (support ())) . y by FUNCT_1:def 3;
consider f being FinSequence of COMPLEX such that
A7: Product () = Product f and
A8: f = () * (canFS (support ())) by NAT_3:def 5;
( rng () c= NAT & rng f c= rng () ) by ;
then A9: rng f c= NAT ;
support () c= dom () by PRE_POLY:37;
then A10: y in dom f by ;
reconsider f = f as FinSequence of NAT by ;
(PFactors n) . p = p by ;
then f . y = p by ;
then p in rng f by ;
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 ; :: thesis: verum