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

proof

let n be 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:6
.= (z GeoSeq) . (n + 1) by Def1 ;
:: thesis: verum

end;

z |^ 0 = 1r by COMPLEX1:def 4, NEWTON:4
.= (z GeoSeq) . 0 by Def1 ;
then A2: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A2, A1);
then z |^ n = (z GeoSeq) . n ;
hence ( w = z |^ n iff w = (z GeoSeq) . n ) ; :: thesis: verum