let a be real number ; :: 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)
defpred S₁[ natural number ] means (1 / a) |^ $1 = 1 / (a |^ $1);
A1: for m being natural number st S₁[m] holds
S₁[m + 1]

proof

let m be natural number ; :: 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 / a) GeoSeq) . 0 by Def1
.= 1 / 1 by Th4
.= 1 / ((a GeoSeq) . 0) by Th4
.= 1 / (a |^ 0) by Def1 ;
then A2: S₁[ 0 ] ;
for m being natural number holds S₁[m] from NAT_1:sch 2(A2, A1);
hence (1 / a) |^ n = 1 / (a |^ n) ; :: thesis: verum