set s0 = InvShift 2;
let a, b be Element of COMPLEX ; :: 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 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_LinearFunc ex R being C_RestFunc 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_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)) ) ) ) and
A7: ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc 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_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 A6;
consider L being C_LinearFunc, R being C_RestFunc 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_LinearFunc ex R being C_RestFunc 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_LinearFunc, R1 being C_RestFunc 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 :: thesis: for n being Nat holds (g (#) s0) . n = g / (n + 2)
let n be 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 :: thesis: for n being Element of NAT holds 0 <> (g (#) s0) . n
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; :: thesis: verum
end;
then A20: g (#) s0 is non-zero 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 non-zero 0 -convergent Complex_Sequence by A20, Def1;
A21: for n being Nat ex x being Complex st
( x in N & x in N1 & h . n = x - z0 )
proof
let n be Nat; :: thesis: ex x being Complex st
( x in N & x in N1 & h . n = x - z0 )
reconsider g0 = g / (n + 2) as Complex ;
take x = z0 + g0; :: thesis: ( x in N & x in N1 & h . n = x - z0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then A22: g / (n + 2) < g / 1 by A17, XREAL_1:76;
|.((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 :: thesis: for z being Complex st z in N & z in N1 holds
(a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0))
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))
reconsider t0 = z0, t = z as Element of COMPLEX by XCMPLX_0:def 2;
(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 * (t - t0)) + (R /. (t - t0)) = (L1 /. (t - t0)) + (R1 /. (t - t0)) 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;
A27: a - b in COMPLEX by XCMPLX_0:def 2;
now :: thesis: for n being Nat holds a - b = (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n
dom R1 = COMPLEX by PARTFUN1:def 2;
then A28: rng h c= dom R1 ;
dom R = COMPLEX by PARTFUN1:def 2;
then A29: rng h c= dom R ;
let n be Nat; :: thesis: a - b = (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n
A30: n in NAT by ORDINAL1:def 12;
then A31: h . n <> 0c by COMSEQ_1:4;
ex x being Complex st
( x in N & x in N1 & h . n = x - z0 ) by A21;
then (a * (h . n)) + (R /. (h . n)) = (b * (h . n)) + (R1 /. (h . n)) by A24;
then A32: ((a * (h . n)) / (h . n)) + ((R /. (h . n)) / (h . n)) = ((b * (h . n)) + (R1 /. (h . n))) / (h . n) by XCMPLX_1:62;
A33: (b * (h . n)) / (h . n) = b * ((h . n) / (h . n))
.= b * 1 by A31, XCMPLX_1:60
.= b ;
A34: (R1 /. (h . n)) / (h . n) = (R1 /. (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A30, A28, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ;
A35: (a * (h . n)) / (h . n) = a * ((h . n) / (h . n))
.= a * 1 by A31, XCMPLX_1:60
.= a ;
(R /. (h . n)) / (h . n) = (R /. (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A30, A29, FUNCT_2:109
.= ((h ") (#) (R /* h)) . n by VALUED_1:5 ;
hence a - b = (((h ") (#) (R1 /* h)) . n) + (- (((h ") (#) (R /* h)) . n)) by A32, A35, A33, A34
.= (((h ") (#) (R1 /* h)) . n) + ((- ((h ") (#) (R /* h))) . n) by VALUED_1:8
.= (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n by A30, 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, A27;
then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = a - b by CFCONT_1:28;
A37: ( (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 A36, A37, COMSEQ_2:26;
hence a = b ; :: thesis: verum