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 )
X: z in COMPLEX by XCMPLX_0:def 2;
z |^ 1 = z by NEWTON:10;
then A2: (z ExpSeq ) . 1 = z / (1 !c ) by Def8
.= z / 1 by Th37, NEWTON:19
.= z ;
A3: (z ExpSeq ) . 0 = (z |^ 0 ) / (0 !c ) by Def8
.= 1r by Th1, X, COMSEQ_3:11 ;
|.(z |^ n).| = |.z.| |^ n

proof

defpred S₁[ Element of NAT ] means |.(z |^ $1).| = |.z.| |^ $1;
|.(z |^ 0 ).| = 1 by COMPLEX1:134, COMSEQ_3:def 1;
then A4: S₁[ 0 ] by NEWTON:9;
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:151
.= |.z.| |^ (k + 1) by NEWTON:11 ;
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