let a, b be Complex; :: thesis:
assume that
A5: 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)) ) ) ) and
A6: ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LINEAR ex R being C_REST st
( b = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) ; :: thesis:
consider N being Neighbourhood of z0 such that
A7: ( 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 A5;
consider L being C_LINEAR, R being C_REST such that
A8: ( a = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A7;
consider N1 being Neighbourhood of z0 such that
A9: ( N1 c= dom f & ex L being C_LINEAR ex R being C_REST st
( b = L /. 1r & ( for z being Complex st z in N1 holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) by A6;
consider L1 being C_LINEAR, R1 being C_REST such that
A10: ( b = L1 /. 1r & ( for z being Complex st z in N1 holds
(f /. z) - (f /. z0) = (L1 /. (z - z0)) + (R1 /. (z - z0)) ) ) by A9;
consider a1 being Complex such that
A11: for b being Complex holds L /. b = a1 * b by Def4;
consider b1 being Complex such that
A12: for b being Complex holds L1 /. b = b1 * b by Def4;
A13: a = a1 * 1r by A8, A11;

A14: now

let z be Complex; :: thesis:
assume A15: ( z in N & z in N1 ) ; :: thesis:
then A16: (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A8;
(L /. (z - z0)) + (R /. (z - z0)) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A10, A15, A16;
then (a1 * (z - z0)) + (R /. (z - z0)) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A11;
then ((a1 * 1r ) * (z - z0)) + (R /. (z - z0)) = ((b1 * 1r ) * (z - z0)) + (R1 /. (z - z0)) by A12;
hence (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) by A10, A12, A13; :: thesis:

end;

consider N0 being Neighbourhood of z0 such that
A17: ( N0 c= N & N0 c= N1 ) by Th10;
consider g being Real such that
A18: ( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= N0 ) by Def5;
deffunc H₁( Element of NAT ) -> Element of REAL = 1 / ($1 + 2);
set s0 = InvShift 2;
reconsider s0 = InvShift 2 as Complex_Sequence ;
A20: ( s0 is convergent & lim s0 = 0 ) by Th3;
set s1 = g (#) s0;
A21: ( g (#) s0 is convergent & lim (g (#) s0) = g * 0 ) by A20, COMSEQ_2:18;

A22: now

let n be Element of NAT ; :: thesis:
thus (g (#) s0) . n = g * (s0 . n) by VALUED_1:6
.= g * (1 / (n + 2)) by Def2
.= g / (n + 2) ; :: thesis:

end;

now

let n be Element of NAT ; :: thesis:
(g (#) s0) . n = g / (n + 2) by A22;
hence 0 <> (g (#) s0) . n by A18, XREAL_1:141; :: thesis:

end;

then A23: g (#) s0 is non-zero by COMSEQ_1:4;
reconsider h = g (#) s0 as convergent_to_0 Complex_Sequence by A21, A23, Def1;
A24: for n being Element of NAT ex x being Complex st
( x in N & x in N1 & h . n = x - z0 )

proof

let n be Element of NAT ; :: thesis:
g / (n + 2) in REAL ;
then reconsider g0 = g / (n + 2) as Complex by NUMBERS:11;
0 + 1 < (n + 1) + 1 by XREAL_1:8;
then A26: g / (n + 2) < g / 1 by A18, XREAL_1:78;
A27: |.((z0 + g0) - z0).| = g / (n + 2) by A18, ABSVALUE:def 1;
take x = z0 + g0; :: thesis:
x in { y where y is Complex : |.(y - z0).| < g } by A26, A27;
then x in N0 by A18;
hence ( x in N & x in N1 & h . n = x - z0 ) by A17, A22; :: thesis:

end;

A28: now

let n be Nat; :: thesis:
X: n in NAT by ORDINAL1:def 13;
then ex x being Complex st
( x in N & x in N1 & h . n = x - z0 ) by A24;
then A29: (a * (h . n)) + (R /. (h . n)) = (b * (h . n)) + (R1 /. (h . n)) by A14;
A30: h . n <> 0c by COMSEQ_1:4, X;
A31: ((a * (h . n)) / (h . n)) + ((R /. (h . n)) / (h . n)) = ((b * (h . n)) + (R1 /. (h . n))) / (h . n) by A29, XCMPLX_1:63;
A32: (a * (h . n)) / (h . n) = a * ((h . n) / (h . n))
.= a * 1 by A30, XCMPLX_1:60
.= a ;
A33: (b * (h . n)) / (h . n) = b * ((h . n) / (h . n))
.= b * 1 by A30, XCMPLX_1:60
.= b ;
dom R = COMPLEX by PARTFUN1:def 4;
then A34: rng h c= dom R ;
dom R1 = COMPLEX by PARTFUN1:def 4;
then A35: rng h c= dom R1 ;
A36: (R /. (h . n)) / (h . n) = (R /. (h . n)) * ((h " ) . n) by VALUED_1:10
.= ((R /* h) . n) * ((h " ) . n) by A34, FUNCT_2:186, X
.= ((h " ) (#) (R /* h)) . n by VALUED_1:5 ;
(R1 /. (h . n)) / (h . n) = (R1 /. (h . n)) * ((h " ) . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h " ) . n) by A35, FUNCT_2:185, X
.= ((h " ) (#) (R1 /* h)) . n by VALUED_1:5 ;
hence a - b = (((h " ) (#) (R1 /* h)) . n) + (- (((h " ) (#) (R /* h)) . n)) by A31, A32, A33, A36
.= (((h " ) (#) (R1 /* h)) . n) + ((- ((h " ) (#) (R /* h))) . n) by VALUED_1:8
.= (((h " ) (#) (R1 /* h)) + (- ((h " ) (#) (R /* h)))) . n by VALUED_1:1, X ;
:: thesis:

end;

then A37: ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;
(((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1 = a - b by A28;
then A38: lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) = a - b by A37, CFCONT_1:50;
A39: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 ) by Def3;
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by Def3;
then a - b = 0 - 0 by A38, A39, COMSEQ_2:26;
hence a = b ; :: thesis: