let e be Element of F_Complex ; :: thesis: for n being non empty Nat holds (power F_Complex ) . e,n = e |^ n
defpred S₁[ Nat] means (power F_Complex ) . e,$1 = e |^ $1;
(power F_Complex ) . e,1 = e by GROUP_1:98;
then A1: S₁[1] by NEWTON:10;

A2: now

let n be non empty Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider n' = n as Element of NAT by ORDINAL1:def 13;
reconsider p = (power F_Complex ) . e,n' as Element of F_Complex ;
assume A3: S₁[n] ; :: thesis: S₁[n + 1]
(power F_Complex ) . e,(n + 1) = p * e by GROUP_1:def 8
.= e |^ (n + 1) by A3, NEWTON:11 ;
hence S₁[n + 1] ; :: thesis: verum

end;

thus for n being non empty Nat holds S₁[n] from NAT_1:sch 10(A1, A2); :: thesis: verum