let x, y be Complex; :: thesis: for s being natural Number holds (x * y) |^ s = (x |^ s) * (y |^ s)
let s be natural Number ; :: thesis: (x * y) |^ s = (x |^ s) * (y |^ s)
reconsider x = x, y = y as Element of COMPLEX by XCMPLX_0:def 2;
(x |^ s) * (y |^ s) = Product (s |-> (x * y)) by RVSUM_1:113;
hence (x * y) |^ s = (x |^ s) * (y |^ s) ; :: thesis: verum