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