for m, n being non zero Nat st m,n are_coprime holds
TSqFactors (m * n) = (TSqFactors m) + (TSqFactors n)