theorem :: MOEBIUS2:49

for n being non zero Nat holds TSqFactors n = (SqFactors n) |^ 2