let z be Element of F_Real; :: thesis: ( z <> 0. F_Real implies for n being Nat holds |.(power (z,n)).| = |.z.| to_power n )
defpred S₁[ Nat] means |.(power (z,$1)).| = |.z.| to_power $1;
assume A1: z <> 0. F_Real ; :: thesis: for n being Nat holds |.(power (z,n)).| = |.z.| to_power n
A2: for n being Nat st S₁[n] holds
S₁[n + 1]

proof

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume A3: |.(power (z,n)).| = |.z.| to_power n ; :: thesis: S₁[n + 1]
thus |.(power (z,(n + 1))).| = |.(((power F_Real) . (z,n)) * z).| by GROUP_1:def 7
.= (|.z.| to_power n) * (|.z.| to_power 1) by A3, COMPLEX1:65
.= |.z.| to_power (n + 1) by A1, POWER:27 ; :: thesis: verum

end;

|.((power F_Real) . (z,0)).| = |.(z |^ 0).| by BINOM:def 2
.= |.(1_ F_Real).| by BINOM:8
.= 1 by ABSVALUE:def 1
.= |.z.| to_power 0 by POWER:24 ;
then A4: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2); :: thesis: verum