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;
A2: z |^ 1 = z by NEWTON:10;
A3: (z ExpSeq ) . 1 = z / (1 !c ) by A2, Def8
.= z / 1 by Th37, NEWTON:19
.= z ;
A4: (z ExpSeq ) . 0 = (z |^ 0 ) / (0 !c ) by Def8
.= 1r by A1, Th1, COMSEQ_3:11 ;
A5: |.(z |^ n).| = |.z.| |^ n

proof

defpred S₁[ Element of NAT ] means |.(z |^ $1).| = |.z.| |^ $1;
A6: |.(z |^ 0 ).| = 1 by COMPLEX1:134, COMSEQ_3:def 1;
A7: S₁[ 0 ] by A6, NEWTON:9;
A8: 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 A9: |.(z |^ k).| = |.z.| |^ k ; :: thesis: S₁[k + 1]
A10: |.(z |^ (k + 1)).| = |.(z * ((z GeoSeq ) . k)).| by COMSEQ_3:def 1
.= (|.z.| |^ k) * |.z.| by A9, COMPLEX1:151
.= |.z.| |^ (k + 1) by NEWTON:11 ;
thus S₁[k + 1] by A10; :: thesis: verum

end;

A11: for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A7, A8);
thus |.(z |^ n).| = |.z.| |^ n by A11; :: thesis: verum

end;

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