let e be Element of F_Complex; :: thesis: for n being Nat holds (power F_Complex) . (e,n) = e |^ n
defpred S₁[ Nat] means (power F_Complex) . (e,$1) = e |^ $1;

A1: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
reconsider p = (power F_Complex) . (e,n9) as Element of F_Complex ;
assume A2: S₁[n] ; :: thesis: S₁[n + 1]
(power F_Complex) . (e,(n + 1)) = p * e by GROUP_1:def 7
.= e |^ (n + 1) by A2, NEWTON:6 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(power F_Complex) . (e,0) = 1_ F_Complex by GROUP_1:def 7
.= 1 by Def1 ;
then A3: S₁[ 0 ] by NEWTON:4;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A1); :: thesis: verum