theorem :: MOEBIUS3:43

for n being non zero Nat holds n = (TSqF n) * (n div (TSqF n))