let x be Complex; :: thesis: for r being natural Number st x <> 0 holds
(x |^ r) " = (x ") |^ r
let r be natural Number ; :: thesis: ( x <> 0 implies (x |^ r) " = (x ") |^ r )
assume A1: x <> 0 ; :: thesis: (x |^ r) " = (x ") |^ r
reconsider y = x * (x ") as Complex ;
A2: y = x / x by XCMPLX_0:def 9
.= 1 by A1, XCMPLX_1:60 ;
(x |^ r) * ((x ") |^ r) = y |^ r by NEWTON:7
.= 1 by A2, NEWTON:10 ;
hence (x |^ r) " = (x ") |^ r by XCMPLX_1:210; :: thesis: verum