let n0, m0 be natural non zero number ; :: thesis: ( n0,m0 are_relative_prime implies sigma (n0 * m0) = (sigma n0) * (sigma m0) )
assume A1: n0,m0 are_relative_prime ; :: 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, Def5
.= (sigma (1,n0)) * ((Sigma 1) . m0) by Def3
.= (sigma n0) * (sigma m0) by Def3 ; :: thesis: verum