let k be natural number ; :: thesis: Sigma k is multiplicative
for n being natural non zero number holds (Sigma k) . n = Sum ((EXP k) | (NatDivisors n))

proof

let n be natural non zero number ; :: thesis: (Sigma k) . n = Sum ((EXP k) | (NatDivisors n))
thus (Sigma k) . n = sigma k,n by Def3
.= Sum ((EXP k) | (NatDivisors n)) by Def2 ; :: thesis: verum

end;

hence Sigma k is multiplicative by Th34, Th35; :: thesis: verum