consider N being Neighbourhood of z0 such that
A2: N c= dom f and
A3: ex L being C_LinearFunc ex R being C_RestFunc st
for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A1;
consider L being C_LinearFunc, R being C_RestFunc such that
A4: for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A3;
consider a being Complex such that
A5: for d being Complex holds L /. d = a * d by Def4;
take a ; :: thesis: ( a is set & a is Element of COMPLEX & ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) )
L /. 1r = a * 1r by A5
.= a ;
hence ( a is set & a is Element of COMPLEX & ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) ) by A2, A4; :: thesis: verum