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 ;

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 )
;

end;

suppose A1:
x = 0
; :: thesis: ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n )

( 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

end;thus ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n ) :: thesis: verum

proof
end;

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

end;

suppose A3:
n = 0
; :: thesis: ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n )

( 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;.= x |^ n by A3, NEWTON:4 ;

hence ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n ) ; :: thesis: verum

suppose A4:
n > 0
; :: thesis: ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n )

( 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;(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

suppose A6:
x <> 0
; :: thesis: ex x being Real st

( x = z & (power F_Complex) . (z,n) = x |^ n )

( x = z & (power F_Complex) . (z,n) = x |^ n )

defpred S_{1}[ Nat] means (power F_Complex) . (z,$1) = x |^ $1;

A7: for n being Nat st S_{1}[n] holds

S_{1}[n + 1]

.= x #Z 0 by PREPOWER:34

.= x |^ 0 by PREPOWER:36 ;

then A9: S_{1}[ 0 ]
;

for n being Nat holds S_{1}[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;A7: for n being Nat st S

S

proof

(power F_Complex) . (z,0) =
1r
by COMPLFLD:8, GROUP_1:def 7
let n be Nat; :: thesis: ( S_{1}[n] implies S_{1}[n + 1] )

assume A8: S_{1}[n]
; :: thesis: S_{1}[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_{1}[n + 1]
; :: thesis: verum

end;assume A8: S

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

.= x #Z 0 by PREPOWER:34

.= x |^ 0 by PREPOWER:36 ;

then A9: S

for n being Nat holds S

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