let a be Complex; :: thesis: for n being natural Number holds (1 / a) |^ n = 1 / (a |^ n)
let n be natural Number ; :: thesis: (1 / a) |^ n = 1 / (a |^ n)
A1: n is Nat by TARSKI:1;
defpred S₁[ Nat] means (1 / a) |^ $1 = 1 / (a |^ $1);
A2: for m being Nat st S₁[m] holds
S₁[m + 1]

proof

let m be Nat; :: thesis: ( S₁[m] implies S₁[m + 1] )
assume (1 / a) |^ m = 1 / (a |^ m) ; :: thesis: S₁[m + 1]
hence (1 / a) |^ (m + 1) = (1 / (a |^ m)) * (1 / a) by NEWTON:6
.= (1 * 1) / ((a |^ m) * a) by XCMPLX_1:76
.= 1 / (a |^ (m + 1)) by NEWTON:6 ;
:: thesis: verum

end;

(1 / a) |^ 0 = 1 by NEWTON:4
.= 1 / 1
.= 1 / (a |^ 0) by NEWTON:4 ;
then A3: S₁[ 0 ] ;
for m being Nat holds S₁[m] from NAT_1:sch 2(A3, A2);
hence (1 / a) |^ n = 1 / (a |^ n) by A1; :: thesis: verum