let n be non zero Nat; :: thesis: for p being Prime holds not p |^ 2 divides Radical n
let p be Prime; :: thesis: not p |^ 2 divides Radical n
set PR = p |-count (Radical n);
A1: p <> 1 by INT_2:def 4;
assume A2: p |^ 2 divides Radical n ; :: thesis: contradiction
A3: p |-count (Radical n) is non zero Element of NAT
proof
assume p |-count (Radical n) is not non zero Element of NAT ; :: thesis: contradiction
then not p |^ (0 + 1) divides Radical n by A1, NAT_3:def 7;
then not p divides Radical n ;
hence contradiction by A2, Th10; :: thesis: verum
end;
p |-count (Radical n) >= 2
proof
assume p |-count (Radical n) < 2 ; :: thesis: contradiction
then p |-count (Radical n) = 1 by A3, NAT_1:23;
then not p |^ (1 + 1) divides Radical n by A1, NAT_3:def 7;
hence contradiction by A2; :: thesis: verum
end;
then p |-count (Radical n) > 1 by XXREAL_0:2;
hence contradiction by Th61; :: thesis: verum