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 )
A1: the carrier of F_Complex = COMPLEX by COMPLFLD:def 1;
defpred S₁[ Element of NAT ] means ex f being Function of COMPLEX ,COMPLEX st
( f = FPower x,$1 & f is_continuous_on COMPLEX );
A2: 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;

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] )
given f being Function of COMPLEX ,COMPLEX such that A4: f = FPower x,n and
A5: f is_continuous_on COMPLEX ; :: thesis: S₁[n + 1]
reconsider g = FPower x,(n + 1) as Function of COMPLEX ,COMPLEX by A1;
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
consider f1 being Function of COMPLEX ,COMPLEX such that
A6: f1 = FPower x,n and
A7: FPower x,(n + 1) = f1 (#) (id COMPLEX ) by Th70;
thus g is_continuous_on COMPLEX by A4, A5, A6, A7, Th63, CFCONT_1:65; :: thesis: verum

end;

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