let z be Element of F_Complex; :: thesis: ( z <> 0. F_Complex implies for n being Nat holds |.(power (z,n)).| = |.z.| to_power n )
defpred S1[ Nat] means |.(power (z,$1)).| = |.z.| to_power $1;
assume z <> 0. F_Complex ; :: thesis: for n being Nat holds |.(power (z,n)).| = |.z.| to_power n
then A1: |.z.| <> 0 by COMPLFLD:58;
A2: |.z.| >= 0 by COMPLEX1:46;
A3: for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[n + 1] )
assume A4: |.(power (z,n)).| = |.z.| to_power n ; :: thesis: S1[n + 1]
thus |.(power (z,(n + 1))).| = |.(((power F_Complex) . (z,n)) * z).| by GROUP_1:def 7
.= (|.z.| to_power n) * |.z.| by A4, COMPLFLD:71
.= (|.z.| to_power n) * (|.z.| to_power 1) by POWER:25
.= |.z.| to_power (n + 1) by A1, A2, POWER:27 ; :: thesis: verum
end;
|.((power F_Complex) . (z,0)).| = 1 by COMPLEX1:48, COMPLFLD:8, GROUP_1:def 7
.= |.z.| to_power 0 by POWER:24 ;
then A5: S1[ 0 ] ;
thus for n being Nat holds S1[n] from NAT_1:sch 2(A5, A3); :: thesis: verum