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

proof

let n be non zero Nat; :: 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