consider N being Neighbourhood of z0 such that
A2: N c= dom f and
A3: ex L being C_LINEAR ex R being C_REST st
for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A1, Def6;
consider L being C_LINEAR, R being C_REST 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: ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST 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 ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST 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