let n be Element of NAT ; :: thesis: for z being complex number holds
( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
let z be complex number ; :: thesis: ( (z ExpSeq) . 1 = z & (z ExpSeq) . 0 = 1r & |.(z |^ n).| = |.z.| |^ n )
A1: z in COMPLEX by XCMPLX_0:def 2;
z |^ 1 = z by NEWTON:5;
then A2: (z ExpSeq) . 1 = z / (1 !) by Def8
.= z by NEWTON:13 ;
A3: (z ExpSeq) . 0 = (z |^ 0) / (0 !) by Def8
.= 1r by A1, Th1, COMSEQ_3:11 ;
|.(z |^ n).| = |.z.| |^ n

proof

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

proof

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

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A5);
hence |.(z |^ n).| = |.z.| |^ n ; :: thesis: verum

end;

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