theorem MB150: :: MOEBIUS2:44

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