let x be Element of F_Complex; :: thesis: for n being Nat ex f being Function of COMPLEX,COMPLEX st
( f = FPower (x,n) & f is_continuous_on COMPLEX )
defpred S₁[ 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 Nat st S₁[n] holds
S₁[n + 1]

proof

let n be 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 Th69;
hence g is_continuous_on COMPLEX by A3, Th62, CFCONT_1:43; :: 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 Th66;
hence f is_continuous_on COMPLEX by A1, Th63; :: thesis: verum

end;

thus for n being Nat holds S₁[n] from NAT_1:sch 2(A4, A2); :: thesis: verum