let z be Element of F_Complex ; :: thesis: ( z <> 0. F_Complex implies for n being Element of NAT holds |.((power F_Complex ) . z,n).| = |.z.| to_power n )
defpred S₁[ Element of NAT ] means |.((power F_Complex ) . z,$1).| = |.z.| to_power $1;
assume z <> 0. F_Complex ; :: thesis: for n being Element of NAT holds |.((power F_Complex ) . z,n).| = |.z.| to_power n
then A1: |.z.| <> 0 by COMPLFLD:94;
A2: |.z.| >= 0 by COMPLEX1:132;
A3: 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 A4: |.((power F_Complex ) . z,n).| = |.z.| to_power n ; :: thesis: S₁[n + 1]
thus |.((power F_Complex ) . z,(n + 1)).| = |.(((power F_Complex ) . z,n) * z).| by GROUP_1:def 8
.= (|.z.| to_power n) * |.z.| by A4, COMPLFLD:109
.= (|.z.| to_power n) * (|.z.| to_power 1) by POWER:30
.= |.z.| to_power (n + 1) by A1, A2, POWER:32 ; :: thesis: verum

end;

|.((power F_Complex ) . z,0 ).| = 1 by COMPLEX1:134, COMPLFLD:10, GROUP_1:def 8
.= |.z.| to_power 0 by POWER:29 ;
then A5: S₁[ 0 ] ;
thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A5, A3); :: thesis: verum