let k be natural number ; :: thesis: EXP k is multiplicative
for n, m being non zero natural number st n,m are_relative_prime holds
(EXP k) . (n * m) = ((EXP k) . n) * ((EXP k) . m)

proof

let n, m be non zero natural number ; :: thesis: ( n,m are_relative_prime implies (EXP k) . (n * m) = ((EXP k) . n) * ((EXP k) . m) )
assume n,m are_relative_prime ; :: thesis: (EXP k) . (n * m) = ((EXP k) . n) * ((EXP k) . m)
thus (EXP k) . (n * m) = (n * m) |^ k by Def1
.= (n |^ k) * (m |^ k) by NEWTON:12
.= ((EXP k) . n) * (m |^ k) by Def1
.= ((EXP k) . n) * ((EXP k) . m) by Def1 ; :: thesis: verum

end;

hence EXP k is multiplicative by Def5; :: thesis: verum