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

A2: now

let n be Element of 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 8
.= [**((x to_power n) * (x to_power 1)),0 **] by POWER:30
.= [**(x to_power (n + 1)),0 **] by A1, POWER:32 ;
hence S₁[n + 1] ; :: thesis: verum

end;

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