reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ;
set R = cf;
now :: thesis: for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )
let h be non-zero 0 -convergent Complex_Sequence; :: thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )
now :: thesis: for n being Nat holds ((h ") (#) (cf /* h)) . n = 0c
let n be Nat; :: thesis: ((h ") (#) (cf /* h)) . n = 0c
A2: ( rng h c= dom cf & n in NAT ) by ORDINAL1:def 12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109
.= ((h ") . n) * 0c
.= 0c ; :: thesis: verum
end;
then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def 18;
hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; :: thesis: verum
end;
then reconsider R = cf as C_RestFunc by Def3;
set L = cf;
for z being Complex holds cf /. z = 0c * z by XCMPLX_0:def 2, FUNCOP_1:7;
then reconsider L = cf as C_LinearFunc by Def4;
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Complex st rng f = {a1} holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) )
let Z be open Subset of COMPLEX; :: thesis: ( Z c= dom f & ex a1 being Complex st rng f = {a1} implies ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) ) )
assume A3: Z c= dom f ; :: thesis: ( for a1 being Complex holds not rng f = {a1} or ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) ) )
given a1 being Complex such that A4: rng f = {a1} ; :: thesis: ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = 0c ) )
A5: now :: thesis: for x0 being Complex st x0 in dom f holds
f /. x0 = a1
let x0 be Complex; :: thesis: ( x0 in dom f implies f /. x0 = a1 )
assume A6: x0 in dom f ; :: thesis: f /. x0 = a1
then f . x0 in {a1} by A4, FUNCT_1:def 3;
then f /. x0 in {a1} by A6, PARTFUN1:def 6;
hence f /. x0 = a1 by TARSKI:def 1; :: thesis: verum
end;
A7: now :: thesis: for x0 being Complex st x0 in Z holds
f is_differentiable_in x0
let x0 be Complex; :: thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A8: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A9: N c= Z by Th9;
A10: N c= dom f by A3, A9;
A11: for x being Complex holds x - x0 in COMPLEX by XCMPLX_0:def 2;
for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Complex; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5, A10
.= a1 - a1 by A3, A5, A8
.= (L /. (x - x0)) + 0c by FUNCOP_1:7, A11
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7, A11 ;
:: thesis: verum
end;
hence f is_differentiable_in x0 by A10; :: thesis: verum
end;
hence A12: f is_differentiable_on Z by A3, Th15; :: thesis: for x being Complex st x in Z holds
(f `| Z) /. x = 0c
let x0 be Complex; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = 0c )
assume A13: x0 in Z ; :: thesis: (f `| Z) /. x0 = 0c
then A14: f is_differentiable_in x0 by A7;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) ;
then consider N being Neighbourhood of x0 such that
A15: N c= dom f ;
A16: for x being Complex st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Complex; :: thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A17: x - x0 in COMPLEX by XCMPLX_0:def 2;
assume x in N ; :: thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5, A15
.= a1 - a1 by A3, A5, A13
.= (L /. (x - x0)) + 0c by FUNCOP_1:7, A17
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7, A17 ;
:: thesis: verum
end;
thus (f `| Z) /. x0 = diff (f,x0) by A12, A13, Def12
.= L /. 1r by A14, A15, A16, Def7
.= 0c ; :: thesis: verum