let a, b be Complex; :: thesis: for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Complex st x in Z holds
f /. x = (a * x) + b ) holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = a ) )
let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Complex st x in Z holds
f /. x = (a * x) + b ) holds
( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = a ) )
let Z be open Subset of COMPLEX; :: thesis: ( Z c= dom f & ( for x being Complex st x in Z holds
f /. x = (a * x) + b ) implies ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = a ) ) )
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: ( n in NAT & rng h c= dom cf ) 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;
assume that
A3: Z c= dom f and
A4: for x being Complex st x in Z holds
f /. x = (a * x) + b ; :: thesis: ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = a ) )
deffunc H₁( Complex) -> Element of COMPLEX = In ((a * $1),COMPLEX);
consider L being Function of COMPLEX,COMPLEX such that
A5: for x being Element of COMPLEX holds L . x = H₁(x) from FUNCT_2:sch 4();
for z being Complex holds L /. z = a * z

proof

let z be Complex; :: thesis: L /. z = a * z
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
L . z = H₁(z) by A5;
hence L /. z = a * z ; :: thesis: verum

end;

then reconsider L = L as C_LinearFunc by Def4;

A6: 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 A7: x0 in Z ; :: thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A8: N c= Z by Th9;
A9: 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)) )
A10: 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) = ((a * x) + b) - (f /. x0) by A4, A8
.= ((a * x) + b) - ((a * x0) + b) by A4, A7
.= H₁(x - x0) + 0c
.= (L /. (x - x0)) + 0c by A5, A10
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7, A10 ;
:: thesis: verum

end;

N c= dom f by A3, A8;
hence f is_differentiable_in x0 by A9; :: thesis: verum

end;

hence A11: f is_differentiable_on Z by A3, Th15; :: thesis: for x being Complex st x in Z holds
(f `| Z) /. x = a
let x0 be Complex; :: thesis: ( x0 in Z implies (f `| Z) /. x0 = a )
assume A12: x0 in Z ; :: thesis: (f `| Z) /. x0 = a
then consider N being Neighbourhood of x0 such that
A13: N c= Z by Th9;
A14: 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)) )
A15: 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) = ((a * x) + b) - (f /. x0) by A4, A13
.= ((a * x) + b) - ((a * x0) + b) by A4, A12
.= H₁(x - x0) + 0c
.= (L /. (x - x0)) + 0c by A5, A15
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7, A15 ;
:: thesis: verum

end;

A16: N c= dom f by A3, A13;
A17: f is_differentiable_in x0 by A6, A12;
thus (f `| Z) /. x0 = diff (f,x0) by A11, A12, Def12
.= L /. 1r by A17, A16, A14, Def7
.= H₁( 1r ) by A5
.= a ; :: thesis: verum