let n be non zero Nat; :: thesis: n = (SquarefreePart n) * ((SqF n) ^2)
(SqF n) |^ 2 divides n by Skup;
then TSqF n divides n by Cosik;
then n = (TSqF n) * (n div (TSqF n)) by NAT_D:3
.= ((SqF n) |^ 2) * (n div (TSqF n)) by Cosik
.= ((SqF n) ^2) * (n div (TSqF n)) by NEWTON:81 ;
hence n = (SquarefreePart n) * ((SqF n) ^2) ; :: thesis: verum