let a, b be Complex; 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; 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; ( 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;
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
; ( f is_differentiable_on Z & ( for x being Complex st x in Z holds
(f `| Z) /. x = a ) )
deffunc H1( 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 = H1(x)
from FUNCT_2:sch 4();
for z being Complex holds L /. z = a * z
then reconsider L = L as C_LinearFunc by Def4;
hence A11:
f is_differentiable_on Z
by A3, Th15; for x being Complex st x in Z holds
(f `| Z) /. x = a
let x0 be Complex; ( x0 in Z implies (f `| Z) /. x0 = a )
assume A12:
x0 in Z
; (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))
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
.=
H1( 1r )
by A5
.=
a
; verum