let n, m be non zero Nat; :: thesis: ( m ^2 divides SquarefreePart n implies m = 1 )
assume A0: m ^2 divides SquarefreePart n ; :: thesis: m = 1
assume m <> 1 ; :: thesis: contradiction
then consider p being Prime such that
A1: p divides m by MOEBIUS1:5;
( p in NAT & m in NAT ) by ORDINAL1:def 12;
then p ^2 divides m ^2 by A1, PYTHTRIP:6;
then p ^2 divides SquarefreePart n by A0, NAT_D:4;
then p |^ 2 divides SquarefreePart n by NEWTON:81;
then 1 + 1 <= p |-count (SquarefreePart n) by MOEBIUS2:40;
hence contradiction by MOEBIUS1:24, NAT_1:13; :: thesis: verum