let k be non zero natural number ; :: thesis: ( not k is square-containing implies Radical k = k )
assume A1: not k is square-containing ; :: thesis: Radical k = k
for i being set st i in SetPrimes holds
(PFactors k) . i = (ppf k) . i

proof

let i be set ; :: thesis: ( i in SetPrimes implies (PFactors k) . i = (ppf k) . i )
assume i in SetPrimes ; :: thesis: (PFactors k) . i = (ppf k) . i
then reconsider p = i as prime Element of NAT by NEWTON:def 6;

per cases ( p in support (pfexp k) or not p in support (pfexp k) ) ;

suppose A2: p in support (pfexp k) ; :: thesis: (PFactors k) . i = (ppf k) . i

A3: p <> 1 by INT_2:def 4;
p |-count k <> 0

proof

assume p |-count k = 0 ; :: thesis: contradiction
then not p divides k by A3, NAT_3:27;
hence contradiction by A2, NAT_3:36; :: thesis: verum

end;

then A4: p |-count k >= 1 by NAT_1:14;
p |-count k <= 1 by A1, Th24;
then p |-count k = 1 by A4, XXREAL_0:1;
then (ppf k) . p = p |^ 1 by A2, NAT_3:def 9
.= p by NEWTON:5 ;
hence (PFactors k) . i = (ppf k) . i by A2, Def6; :: thesis: verum

end;

suppose A5: not p in support (pfexp k) ; :: thesis: (PFactors k) . i = (ppf k) . i

then not p in support (PFactors k) by Def6;
then A6: (PFactors k) . p = 0 by PRE_POLY:def 7;
not p in support (ppf k) by A5, NAT_3:def 9;
hence (PFactors k) . i = (ppf k) . i by A6, PRE_POLY:def 7; :: thesis: verum

end;

end;

end;

then PFactors k = ppf k by PBOOLE:3;
hence Radical k = k by NAT_3:61; :: thesis: verum