reconsider n = n as Element of NAT by ORDINAL1:def 13;
defpred S₁[ Element of NAT ] means z |^ $1 = (z GeoSeq ) . $1;
let w be Element of COMPLEX ; :: thesis: ( w = z #N n iff w = (z GeoSeq ) . n )
A1: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
hence z |^ (n + 1) = ((z GeoSeq ) . n) * z by NEWTON:11
.= (z GeoSeq ) . (n + 1) by Def1 ;
:: thesis: verum

end;

z |^ 0 = 1r by COMPLEX1:def 7, NEWTON:9
.= (z GeoSeq ) . 0 by Def1 ;
then A2: S₁[ 0 ] ;
for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A2, A1);
then z |^ n = (z GeoSeq ) . n ;
hence ( w = z #N n iff w = (z GeoSeq ) . n ) ; :: thesis: verum