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