for n being non zero Nat holds n = (SquarefreePart n) * ((SqF n) ^2)