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 S1[ 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 S1[n] holds
S1[n + 1]
proof
let n be Nat; :: thesis: ( S1[n] implies S1[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: S1[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: S1[ 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 S1[n] from NAT_1:sch 2(A4, A2); :: thesis: verum