let n be Nat; :: thesis: for z being Complex holds
( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
let z be Complex; :: thesis: ( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
z |^ 1 = z ;
then A1: (z ExpSeq) . 1 = z / (1 !) by Def4
.= z by NEWTON:13 ;
A2: (z ExpSeq) . 0 = (z |^ 0) / (0 !) by Def4
.= 1r by Th1, COMSEQ_3:11 ;
|.(z |^ n).| = |.z.| |^ n

proof

defpred S₁[ Nat] means |.(z |^ $1).| = |.z.| |^ $1;
|.(z |^ 0).| = 1 by COMPLEX1:48, COMSEQ_3:def 1;
then A3: S₁[ 0 ] by NEWTON:4;
A4: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A4);
hence |.(z |^ n).| = |.z.| |^ n ; :: thesis: verum

end;

hence ( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n ) by A1, A2; :: thesis: verum