let a be Complex; :: thesis: for n being Nat holds |.a.| |^ n = |.(a |^ n).|
let n be Nat; :: thesis: |.a.| |^ n = |.(a |^ n).|
defpred S₁[ Nat] means |.a.| |^ $1 = |.(a |^ $1).|;
A1: S₁[ 0 ]

proof

|.a.| |^ 0 = |.1.| by NEWTON:4
.= |.(a |^ 0).| by NEWTON:4 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume B1: |.a.| |^ k = |.(a |^ k).| ; :: thesis: S₁[k + 1]
|.(a |^ (k + 1)).| = |.(a * (a |^ k)).| by NEWTON:6
.= |.a.| * (|.a.| |^ k) by B1, COMPLEX1:65 ;
hence S₁[k + 1] by NEWTON:6; :: thesis: verum

end;

for l being Nat holds S₁[l] from NAT_1:sch 2(A1, A2);
hence |.a.| |^ n = |.(a |^ n).| ; :: thesis: verum