let n be Element of NAT ; :: thesis: for z being Element of F_Complex st z is Real holds
ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )
let z be Element of F_Complex; :: thesis: ( z is Real implies ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n ) )
assume z is Real ; :: thesis: ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )
then reconsider x = z as Real ;

per cases ( x = 0 or x <> 0 ) ;

suppose A1: x = 0 ; :: thesis: ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )

then A2: z = 0. F_Complex by COMPLFLD:def 1;
thus ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n ) :: thesis: verum

proof

per cases ( n = 0 or n > 0 ) ;

suppose A3: n = 0 ; :: thesis: ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )

then (power F_Complex) . (z,n) = 1 by COMPLFLD:8, GROUP_1:def 7
.= x |^ n by A3, NEWTON:4 ;
hence ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n ) ; :: thesis: verum

end;

suppose A4: n > 0 ; :: thesis: ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )

then A5: n >= 0 + 1 by NAT_1:13;
(power F_Complex) . (z,n) = 0. F_Complex by A2, A4, VECTSP_1:36
.= x |^ n by A1, A5, COMPLFLD:7, NEWTON:11 ;
hence ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n ) ; :: thesis: verum

end;

end;

end;

end;

suppose A6: x <> 0 ; :: thesis: ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n )

defpred S₁[ Nat] means (power F_Complex) . (z,$1) = x |^ $1;
A7: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A8: S₁[n] ; :: thesis: S₁[n + 1]
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
(power F_Complex) . (z,(n + 1)) = ((power F_Complex) . (z,nn)) * z by GROUP_1:def 7
.= (x #Z n) * x by A8, PREPOWER:36
.= (x #Z n) * (x #Z 1) by PREPOWER:35
.= x #Z (n + 1) by A6, PREPOWER:44
.= x |^ (n + 1) by PREPOWER:36 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(power F_Complex) . (z,0) = 1r by COMPLFLD:8, GROUP_1:def 7
.= x #Z 0 by PREPOWER:34
.= x |^ 0 by PREPOWER:36 ;
then A9: S₁[ 0 ] ;
for n being Nat holds S₁[n] from NAT_1:sch 2(A9, A7);
then (power F_Complex) . (z,n) = x |^ n ;
hence ex x being Real st
( x = z & (power F_Complex) . (z,n) = x |^ n ) ; :: thesis: verum

end;

end;