let s be Nat; :: thesis: for x, y being complex number holds (x * y) |^ s = (x |^ s) * (y |^ s)
let x, y be complex 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