let k be Nat; :: thesis: Sigma k is multiplicative

for n being non zero Nat holds (Sigma k) . n = Sum ((EXP k) | (NatDivisors n))

for n being non zero Nat holds (Sigma k) . n = Sum ((EXP k) | (NatDivisors n))

proof

hence
Sigma k is multiplicative
by Th34, Th35; :: thesis: verum
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;thus (Sigma k) . n = sigma (k,n) by Def3

.= Sum ((EXP k) | (NatDivisors n)) by Def2 ; :: thesis: verum