let x be Element of F_Complex ; :: thesis: for n being Element of NAT ex f being Function of COMPLEX ,COMPLEX st
( f = FPower x,n & f is_continuous_on COMPLEX )
defpred S₁[ Element of NAT ] means ex f being Function of COMPLEX ,COMPLEX st
( f = FPower x,$1 & f is_continuous_on COMPLEX );
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
A2: 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] )
reconsider g = FPower x,(n + 1) as Function of COMPLEX ,COMPLEX by A1;
given f being Function of COMPLEX ,COMPLEX such that A3: ( f = FPower x,n & f is_continuous_on COMPLEX ) ; :: thesis: S₁[n + 1]
take g ; :: thesis: ( g = FPower x,(n + 1) & g is_continuous_on COMPLEX )
thus g = FPower x,(n + 1) ; :: thesis: g is_continuous_on COMPLEX
ex f1 being Function of COMPLEX ,COMPLEX st
( f1 = FPower x,n & FPower x,(n + 1) = f1 (#) (id COMPLEX ) ) by Th70;
hence g is_continuous_on COMPLEX by A3, Th63, CFCONT_1:65; :: thesis: verum

end;

A4: S₁[ 0 ]

proof

reconsider f = FPower x,0 as Function of COMPLEX ,COMPLEX by A1;
take f ; :: thesis: ( f = FPower x,0 & f is_continuous_on COMPLEX )
thus f = FPower x,0 ; :: thesis: f is_continuous_on COMPLEX
f = the carrier of F_Complex --> x by Th67;
hence f is_continuous_on COMPLEX by A1, Th64; :: thesis: verum

end;

thus for n being Element of NAT holds S₁[n] from NAT_1:sch 1(A4, A2); :: thesis: verum