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 Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A1, Def6;
consider L being C_LinearFunc, R being C_RestFunc such that
A4: for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A3;
consider a being Element of COMPLEX such that
A5: for d being Element of COMPLEX holds L /. d = a * d by Def4;
take a ; :: thesis: 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 Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )
L /. 1r = a * 1r by A5
.= a ;
hence 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 Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) by A2, A4; :: thesis: verum