theorem MB150T: :: MOEBIUS2:52

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