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

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