let k be non zero Nat; :: thesis:
assume A1: k is square-free ; :: thesis:
for i being object st i in SetPrimes holds
(PFactors k) . i = (ppf k) . i

proof

let i be object ; :: thesis:
assume i in SetPrimes ; :: thesis:
then reconsider p = i as prime Element of NAT by NEWTON:def 6;

per cases ;

suppose A2: p in support (pfexp k) ; :: thesis:

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

proof

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

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 ;
hence (PFactors k) . i = (ppf k) . i by A2, Def6; :: thesis:

end;

suppose A5: not p in support (pfexp k) ; :: thesis:

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:

end;

end;

end;

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