set s0 = InvShift 2;
let a, b be Complex; :: 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)) ) ) ) & 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)) ) ) ) implies a = b )
assume that
A6: 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
A7: 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: a = b
consider N being Neighbourhood of z0 such that
N c= dom f and
A8: 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 A6;
consider L being C_LINEAR, R being C_REST such that
A9: a = L /. 1r and
A10: for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A8;
consider a1 being Complex such that
A11: for b being Complex holds L /. b = a1 * b by Def4;
consider N1 being Neighbourhood of z0 such that
N1 c= dom f and
A12: 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 A7;
consider L1 being C_LINEAR, R1 being C_REST such that
A13: b = L1 /. 1r and
A14: for z being Complex st z in N1 holds
(f /. z) - (f /. z0) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A12;
consider b1 being Complex such that
A15: for b being Complex holds L1 /. b = b1 * b by Def4;
reconsider s0 = InvShift 2 as Complex_Sequence ;
consider N0 being Neighbourhood of z0 such that
A16: ( N0 c= N & N0 c= N1 ) by Lm1;
consider g being Real such that
A17: 0 < g and
A18: { y where y is Complex : |.(y - z0).| < g } c= N0 by Def5;
set s1 = g (#) s0;

A19: now

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

end;

now

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

end;

then A20: g (#) s0 is non-empty by COMSEQ_1:4;
lim s0 = 0 by Th3;
then lim (g (#) s0) = g * 0 by COMSEQ_2:18;
then reconsider h = g (#) s0 as convergent_to_0 Complex_Sequence by A20, Def1;
A21: 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: ex x being Complex st
( x in N & x in N1 & h . n = x - z0 )
g / (n + 2) in REAL ;
then reconsider g0 = g / (n + 2) as Complex by NUMBERS:11;
take x = z0 + g0; :: thesis: ( x in N & x in N1 & h . n = x - z0 )
0 + 1 < (n + 1) + 1 by XREAL_1:8;
then A22: g / (n + 2) < g / 1 by A17, XREAL_1:78;
|.((z0 + g0) - z0).| = g / (n + 2) by A17, ABSVALUE:def 1;
then x in { y where y is Complex : |.(y - z0).| < g } by A22;
then x in N0 by A18;
hence ( x in N & x in N1 & h . n = x - z0 ) by A16, A19; :: thesis: verum

end;

A23: a = a1 * 1r by A9, A11;

A24: now

let z be Complex; :: thesis: ( z in N & z in N1 implies (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) )
assume that
A25: z in N and
A26: z in N1 ; :: thesis: (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0))
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A10, A25;
then (L /. (z - z0)) + (R /. (z - z0)) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A14, A26;
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 A15;
hence (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) by A13, A15, A23; :: thesis: verum

end;

now

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

end;

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