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 A1: z is Real ; :: thesis: ex x being Real st
( x = z & (power F_Complex ) . z,n = x |^ n )
reconsider x = z as Real by A1;

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

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

then A3: 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 A4: 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:10, GROUP_1:def 8
.= x |^ n by A4, NEWTON:9 ;
hence ex x being Real st
( x = z & (power F_Complex ) . z,n = x |^ n ) ; :: thesis: verum

end;

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

then A6: n >= 0 + 1 by NAT_1:13;
(power F_Complex ) . z,n = 0. F_Complex by A3, A5, VECTSP_1:95
.= x |^ n by A2, A6, COMPLFLD:9, NEWTON:16 ;
hence ex x being Real st
( x = z & (power F_Complex ) . z,n = x |^ n ) ; :: thesis: verum

end;

end;

end;

end;

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

defpred S₁[ Element of NAT ] means (power F_Complex ) . z,$1 = x |^ $1;
(power F_Complex ) . z,0 = 1r by COMPLFLD:10, GROUP_1:def 8
.= x #Z 0 by PREPOWER:44
.= x |^ 0 by PREPOWER:46 ;
then A8: S₁[ 0 ] ;
A9: for n being Element of NAT st S₁[n] holds
S₁[n + 1]

proof

let n be Element of NAT ; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A10: S₁[n] ; :: thesis: S₁[n + 1]
(power F_Complex ) . z,(n + 1) = ((power F_Complex ) . z,n) * z by GROUP_1:def 8
.= (x #Z n) * x by A10, PREPOWER:46
.= (x #Z n) * (x #Z 1) by PREPOWER:45
.= x #Z (n + 1) by A7, PREPOWER:54
.= x |^ (n + 1) by PREPOWER:46 ;
hence S₁[n + 1] ; :: thesis: verum

end;

for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A8, A9);
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;