let x be Complex; :: thesis: for s, t being natural Number holds (x |^ s) |^ t = x |^ (s * t)
let s, t be natural 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:112;
hence (x |^ s) |^ t = x |^ (s * t) ; :: thesis: verum