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 S1[ Nat] means |.(z |^ $1).| = |.z.| |^ $1;
|.(z |^ 0).| = 1 by COMPLEX1:48, COMSEQ_3:def 1;
then A3: S1[ 0 ] by NEWTON:4;
A4: for k being Nat st S1[k] holds
S1[k + 1]
proof
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A5: |.(z |^ k).| = |.z.| |^ k ; :: thesis: S1[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 S1[k + 1] ; :: thesis: verum
end;
for n being Nat holds S1[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