let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: for x0 being Complex
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 Complex_Sequence
for c being V8() Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) )
let x0 be Complex; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being convergent_to_0 Complex_Sequence
for c being V8() Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) )
let N be Neighbourhood of x0; :: thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being convergent_to_0 Complex_Sequence
for c being V8() Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) )
assume A1: ( f is_differentiable_in x0 & N c= dom f ) ; :: thesis: for h being convergent_to_0 Complex_Sequence
for c being V8() Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) )
let h be convergent_to_0 Complex_Sequence; :: thesis: for c being V8() Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) )
let c be V8() Complex_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) ) )
assume A2: ( rng c = {x0} & rng (h + c) c= N ) ; :: thesis: ( (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent & diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) )
consider N1 being Neighbourhood of x0 such that
A3: ( N1 c= dom f & ex L being C_LINEAR ex R being C_REST st
for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by A1, Def6;
consider L being C_LINEAR, R being C_REST such that
A4: for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A3;
consider N2 being Neighbourhood of x0 such that
A5: ( N2 c= N & N2 c= N1 ) by Th10;
consider g being Real such that
A6: ( 0 < g & { y where y is Complex : |.(y - x0).| < g } c= N2 ) by Def5;
|.(x0 - x0).| = 0 by COMPLEX1:130;
then x0 in { y where y is Complex : |.(y - x0).| < g } by A6;
then A7: x0 in N2 by A6;
ex n being Element of NAT st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )

proof

A8: c is convergent by CFCONT_1:48;
x0 in rng c by A2, TARSKI:def 1;
then A9: lim c = x0 by CFCONT_1:49;
( h is convergent & lim h = 0 ) by Def1;
then A11: lim (h + c) = 0 + x0 by A8, A9, COMSEQ_2:14
.= x0 ;
h + c is convergent by A8, COMSEQ_2:13;
then consider n being Element of NAT such that
A12: for m being Element of NAT st n <= m holds
|.(((h + c) . m) - x0).| < g by A6, A11, COMSEQ_2:def 5;
A13: rng (c ^\ n) = {x0} by A2, VALUED_0:26;
take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
thus rng (c ^\ n) c= N2 :: thesis: rng ((h + c) ^\ n) c= N2

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in N2 )
assume y in rng (c ^\ n) ; :: thesis: y in N2
hence y in N2 by A7, A13, TARSKI:def 1; :: thesis: verum

end;

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2
then consider m being Element of NAT such that
A14: y = ((h + c) ^\ n) . m by FUNCT_2:190;
n + 0 <= n + m by XREAL_1:9;
then |.(((h + c) . (n + m)) - x0).| < g by A12;
then A15: |.((((h + c) ^\ n) . m) - x0).| < g by NAT_1:def 3;
reconsider y1 = y as Complex by A14;
y1 in { z where z is Complex : |.(z - x0).| < g } by A14, A15;
hence y in N2 by A6; :: thesis: verum

end;

then consider n being Element of NAT such that
A16: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 ) ;
A17: rng (c ^\ n) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom f )
A18: rng (c ^\ n) = rng c by VALUED_0:26;
assume y in rng (c ^\ n) ; :: thesis: y in dom f
then y = x0 by A2, A18, TARSKI:def 1;
then y in N by A5, A7;
hence y in dom f by A1; :: thesis: verum

end;

A19: rng ((h + c) ^\ n) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in dom f )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in dom f
then y in N2 by A16;
then y in N by A5;
hence y in dom f by A1; :: thesis: verum

end;

A20: rng c c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom f )
assume y in rng c ; :: thesis: y in dom f
then y = x0 by A2, TARSKI:def 1;
then y in N by A5, A7;
hence y in dom f by A1; :: thesis: verum

end;

A21: rng (h + c) c= dom f

proof

let y be set ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (h + c) or y in dom f )
assume y in rng (h + c) ; :: thesis: y in dom f
then y in N by A2;
hence y in dom f by A1; :: thesis: verum

end;

A22: for x being Complex st x in N2 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A4, A5;
A23: for k being Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))

proof

let k be Element of NAT ; :: thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
((h + c) ^\ n) . k in rng ((h + c) ^\ n) by FUNCT_2:189;
then A24: ((h + c) ^\ n) . k in N2 by A16;
A25: (((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def 3
.= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by VALUED_1:1
.= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def 3
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def 3
.= (h ^\ n) . k ;
A26: (c ^\ n) . k in rng (c ^\ n) by FUNCT_2:189;
rng (c ^\ n) = rng c by VALUED_0:26;
then (c ^\ n) . k = x0 by A2, A26, TARSKI:def 1;
hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A4, A5, A24, A25; :: thesis: verum

end;

A29: for k being Element of NAT holds (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n))

proof

now

let k be Element of NAT ; :: thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by CFCONT_1:2
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A19, FUNCT_2:186
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A17, FUNCT_2:186
.= (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A23
.= ((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by FUNCT_2:192
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by FUNCT_2:192
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by VALUED_1:1 ; :: thesis: verum

end;

hence for k being Element of NAT holds (f /* ((h + c) ^\ n)) - (f /* (c ^\ n)) = (L /* (h ^\ n)) + (R /* (h ^\ n)) by FUNCT_2:113; :: thesis: verum

end;

A30: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ) is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = L /. 1r )

proof

deffunc H₁( Element of NAT ) -> Element of COMPLEX = (L /. 1r ) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . $1);
consider s1 being Complex_Sequence such that
A31: for k being Element of NAT holds s1 . k = H₁(k) from COMSEQ_1:sch 1();
consider x being Complex such that
A32: for b1 being Complex holds L /. b1 = x * b1 by Def4;
A33: L /. 1r = x * 1r by A32
.= x ;

now

let m be Element of NAT ; :: thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m = s1 . m
A34: (h ^\ n) . m <> 0c by COMSEQ_1:4;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) " ) . m) by VALUED_1:5
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) " ) . m) by VALUED_1:1
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) " ) . m))
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) " ) . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by VALUED_1:5
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by VALUED_1:10
.= ((L /. ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by FUNCT_2:192
.= ((x * ((h ^\ n) . m)) * (((h ^\ n) . m) " )) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by A32
.= (x * (((h ^\ n) . m) * (((h ^\ n) . m) " ))) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m)
.= (x * 1r ) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . m) by A34, XCMPLX_0:def 7
.= s1 . m by A31, A33 ; :: thesis: verum

end;

then A35: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ) = s1 by FUNCT_2:113;

A36: now

let r be Real; :: thesis: ( 0 < r implies ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L /. 1r )) < r )
assume A37: 0 < r ; :: thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L /. 1r )) < r
( ((h ^\ n) " ) (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) " ) (#) (R /* (h ^\ n))) = 0 ) by Def3;
then consider m being Element of NAT such that
A38: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0c ) < r by A37, COMSEQ_2:def 5;
take n1 = m; :: thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L /. 1r )) < r
let k be Element of NAT ; :: thesis: ( n1 <= k implies abs ((s1 . k) - (L /. 1r )) < r )
assume A39: n1 <= k ; :: thesis: abs ((s1 . k) - (L /. 1r )) < r
abs ((s1 . k) - (L /. 1r )) = abs (((L /. 1r ) + (((R /* (h ^\ n)) (#) ((h ^\ n) " )) . k)) - (L /. 1r )) by A31
.= abs (((((h ^\ n) " ) (#) (R /* (h ^\ n))) . k) - 0c ) ;
hence abs ((s1 . k) - (L /. 1r )) < r by A38, A39; :: thesis: verum

end;

hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ) is convergent by A35, COMSEQ_2:def 4; :: thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = L /. 1r
hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " )) = L /. 1r by A35, A36, COMSEQ_2:def 5; :: thesis: verum

end;

A40: N2 c= dom f by A1, A5, XBOOLE_1:1;
A41: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) " ) = ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) (#) ((h ^\ n) " ) by A29
.= (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) " ) by A21, VALUED_0:27
.= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) " ) by A20, VALUED_0:27
.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) " ) by Th23
.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h " ) ^\ n) by Th24
.= (((f /* (h + c)) - (f /* c)) (#) (h " )) ^\ n by Th25 ;
then A42: L /. 1r = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) by A30, CFCONT_1:45;
thus (h " ) (#) ((f /* (h + c)) - (f /* c)) is convergent by A30, A41, CFCONT_1:44; :: thesis: diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c)))
thus diff f,x0 = lim ((h " ) (#) ((f /* (h + c)) - (f /* c))) by A1, A22, A40, A42, Def7; :: thesis: verum