let n0, m0 be non zero Nat; :: thesis: ( n0,m0 are_coprime implies sigma (n0 * m0) = (sigma n0) * (sigma m0) )
assume A1: n0,m0 are_coprime ; :: thesis: sigma (n0 * m0) = (sigma n0) * (sigma m0)
A2: Sigma 1 is multiplicative by Th36;
thus sigma (n0 * m0) = (Sigma 1) . (n0 * m0) by Def3
.= ((Sigma 1) . n0) * ((Sigma 1) . m0) by A1, A2
.= (sigma (1,n0)) * ((Sigma 1) . m0) by Def3
.= (sigma n0) * (sigma m0) by Def3 ; :: thesis: verum