let x be Real; :: thesis: for n being Nat holds |.(x |^ n).| = |.x.| |^ n

let n be Nat; :: thesis: |.(x |^ n).| = |.x.| |^ n

defpred S_{1}[ Nat] means |.(x |^ $1).| = |.x.| |^ $1;

A1: for k being Nat st S_{1}[k] holds

S_{1}[k + 1]

.= 1 by ABSVALUE:def 1 ;

then A3: S_{1}[ 0 ]
by NEWTON:4;

for n being Nat holds S_{1}[n]
from NAT_1:sch 2(A3, A1);

hence |.(x |^ n).| = |.x.| |^ n ; :: thesis: verum

let n be Nat; :: thesis: |.(x |^ n).| = |.x.| |^ n

defpred S

A1: for k being Nat st S

S

proof

|.(x |^ 0).| =
|.1.|
by NEWTON:4
let k be Nat; :: thesis: ( S_{1}[k] implies S_{1}[k + 1] )

assume A2: S_{1}[k]
; :: thesis: S_{1}[k + 1]

|.(x |^ (k + 1)).| = |.(x * (x |^ k)).| by NEWTON:6

.= |.x.| * |.(x |^ k).| by COMPLEX1:65

.= |.x.| |^ (k + 1) by A2, NEWTON:6 ;

hence S_{1}[k + 1]
; :: thesis: verum

end;assume A2: S

|.(x |^ (k + 1)).| = |.(x * (x |^ k)).| by NEWTON:6

.= |.x.| * |.(x |^ k).| by COMPLEX1:65

.= |.x.| |^ (k + 1) by A2, NEWTON:6 ;

hence S

.= 1 by ABSVALUE:def 1 ;

then A3: S

for n being Nat holds S

hence |.(x |^ n).| = |.x.| |^ n ; :: thesis: verum