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

proof

let n be non zero natural 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 Th35, Th34; :: thesis: verum