let x be Real; :: thesis: ( x > 0 implies for n being Nat holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**] )
defpred S₁[ Nat] means (power F_Complex) . ([**x,0**],$1) = [**(x to_power $1),0**];
assume A1: x > 0 ; :: thesis: for n being Nat holds (power F_Complex) . ([**x,0**],n) = [**(x to_power n),0**]

A2: now :: thesis: for n being Nat st S₁[n] holds
S₁[n + 1]

let n be Nat; :: thesis: ( S₁[n] implies S₁[n + 1] )
assume S₁[n] ; :: thesis: S₁[n + 1]
then (power F_Complex) . ([**x,0**],(n + 1)) = [**(x to_power n),0**] * [**x,0**] by GROUP_1:def 7
.= [**((x to_power n) * (x to_power 1)),0**] by POWER:25
.= [**(x to_power (n + 1)),0**] by A1, POWER:27 ;
hence S₁[n + 1] ; :: thesis: verum

end;

(power F_Complex) . ([**x,0**],0) = 1r + (0 * <i>) by COMPLFLD:8, GROUP_1:def 7
.= [**(x to_power 0),0**] by POWER:24 ;
then A3: S₁[ 0 ] ;
thus for n being Nat holds S₁[n] from NAT_1:sch 2(A3, A2); :: thesis: verum