for n0, m0 being non zero Nat st n0,m0 are_coprime holds
sigma (n0 * m0) = (sigma n0) * (sigma m0)