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₁[ Nat] means |.(x |^ $1).| = |.x.| |^ $1;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[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₁[k + 1] ; :: thesis: verum

end;

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