:: CFDIFF_2 semantic presentation
begin
Lm1: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim
proof
let seq be Real_Sequence; ::_thesis: for cseq being Complex_Sequence
for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim
let cseq be Complex_Sequence; ::_thesis: for rlim being real number st seq = cseq & seq is convergent & lim seq = rlim holds
lim cseq = rlim
let rlim be real number ; ::_thesis: ( seq = cseq & seq is convergent & lim seq = rlim implies lim cseq = rlim )
assume A1: ( seq = cseq & seq is convergent & lim seq = rlim ) ; ::_thesis: lim cseq = rlim
reconsider clim = rlim as Element of COMPLEX by XCMPLX_0:def_2;
( cseq is convergent & ( for p being Real st 0 < p holds
ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs ((cseq . m) - clim) < p ) ) by A1, SEQ_2:def_7;
hence lim cseq = rlim by COMSEQ_2:def_6; ::_thesis: verum
end;
Lm2: for seq being Real_Sequence
for cseq being Complex_Sequence
for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim
proof
let seq be Real_Sequence; ::_thesis: for cseq being Complex_Sequence
for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim
let cseq be Complex_Sequence; ::_thesis: for rlim being Real st seq = cseq & cseq is convergent & lim cseq = rlim holds
lim seq = rlim
let rlim be Real; ::_thesis: ( seq = cseq & cseq is convergent & lim cseq = rlim implies lim seq = rlim )
assume that
A1: seq = cseq and
A2: cseq is convergent and
A3: lim cseq = rlim ; ::_thesis: lim seq = rlim
reconsider clim = rlim as Complex ;
A4: now__::_thesis:_for_p_being_real_number_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((seq_._m)_-_rlim).|_<_p
let p be real number ; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p )
assume A5: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p
p is Real by XREAL_0:def_1;
then consider n being Element of NAT such that
A6: for m being Element of NAT st n <= m holds
|.((cseq . m) - clim).| < p by A2, A3, A5, COMSEQ_2:def_6;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p
thus for m being Element of NAT st n <= m holds
|.((seq . m) - rlim).| < p by A1, A6; ::_thesis: verum
end;
seq is convergent by A1, A2;
hence lim seq = rlim by A4, SEQ_2:def_7; ::_thesis: verum
end;
Lm3: for seq being Real_Sequence
for cseq being Complex_Sequence st seq = cseq holds
( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
proof
let seq be Real_Sequence; ::_thesis: for cseq being Complex_Sequence st seq = cseq holds
( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
let cseq be Complex_Sequence; ::_thesis: ( seq = cseq implies ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) ) )
assume A1: seq = cseq ; ::_thesis: ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
thus ( seq is 0 -convergent & seq is non-zero implies ( cseq is 0 -convergent & cseq is non-zero ) ) ::_thesis: ( cseq is 0 -convergent & cseq is non-zero implies ( seq is 0 -convergent & seq is non-zero ) )
proof
assume A2: ( seq is 0 -convergent & seq is non-zero ) ; ::_thesis: ( cseq is 0 -convergent & cseq is non-zero )
then A3: seq is convergent ;
lim seq = 0 by A2;
then A4: lim cseq = 0 by A1, A3, Lm1;
A5: cseq is non-zero by A1, A2;
cseq is convergent by A1, A3;
hence ( cseq is 0 -convergent & cseq is non-zero ) by A5, A4, CFDIFF_1:def_1; ::_thesis: verum
end;
assume A6: ( cseq is 0 -convergent & cseq is non-zero ) ; ::_thesis: ( seq is 0 -convergent & seq is non-zero )
then lim cseq = 0 by CFDIFF_1:def_1;
then A7: lim seq = 0 by A1, A6, Lm2;
thus ( seq is 0 -convergent & seq is non-zero ) by A1, A6, A7, FDIFF_1:def_1; ::_thesis: verum
end;
theorem Th1: :: CFDIFF_2:1
for f being PartFunc of COMPLEX,COMPLEX st f is total holds
( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )
proof
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is total implies ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX ) )
assume f is total ; ::_thesis: ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX )
then dom f = COMPLEX by PARTFUN1:def_2;
hence ( dom (Re f) = COMPLEX & dom (Im f) = COMPLEX ) by COMSEQ_3:def_3, COMSEQ_3:def_4; ::_thesis: verum
end;
Lm4: for seq, cseq being Complex_Sequence st cseq = * (#) seq holds
( seq is non-zero iff cseq is non-zero )
proof
let seq, cseq be Complex_Sequence; ::_thesis: ( cseq = ** (#) seq implies ( seq is non-zero iff cseq is non-zero ) )
assume A1: cseq = ** (#) seq ; ::_thesis: ( seq is non-zero iff cseq is non-zero )
thus ( seq is non-zero implies cseq is non-zero ) by A1, COMSEQ_1:38; ::_thesis: ( cseq is non-zero implies seq is non-zero )
A2: ( ** (#) seq is non-zero implies seq is non-zero )
proof
assume A3: ** (#) seq is non-zero ; ::_thesis: seq is non-zero
now__::_thesis:_for_n_being_Element_of_NAT_holds_seq_._n_<>_0c
let n be Element of NAT ; ::_thesis: seq . n <> 0c
(** (#) seq) . n <> 0c by A3, COMSEQ_1:4;
then ** * (seq . n) <> 0c by VALUED_1:6;
hence seq . n <> 0c ; ::_thesis: verum
end;
hence seq is non-zero by COMSEQ_1:4; ::_thesis: verum
end;
assume cseq is non-zero ; ::_thesis: seq is non-zero
hence seq is non-zero by A1, A2; ::_thesis: verum
end;
Lm5: for seq, cseq being Complex_Sequence st cseq = ** (#) seq holds
( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
proof
let seq, cseq be Complex_Sequence; ::_thesis: ( cseq = ** (#) seq implies ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) ) )
assume A1: cseq = ** (#) seq ; ::_thesis: ( seq is 0 -convergent & seq is non-zero iff ( cseq is 0 -convergent & cseq is non-zero ) )
thus ( seq is 0 -convergent & seq is non-zero implies ( cseq is 0 -convergent & cseq is non-zero ) ) ::_thesis: ( cseq is 0 -convergent & cseq is non-zero implies ( seq is 0 -convergent & seq is non-zero ) )
proof
assume A2: ( seq is 0 -convergent & seq is non-zero ) ; ::_thesis: ( cseq is 0 -convergent & cseq is non-zero )
then lim seq = 0 by CFDIFF_1:def_1;
then A3: lim (** (#) seq) = ** * 0 by A2, COMSEQ_2:18
.= 0 ;
( ** (#) seq is non-zero & ** (#) seq is convergent ) by A2, COMSEQ_1:38;
hence ( cseq is 0 -convergent & cseq is non-zero ) by A1, A3, CFDIFF_1:def_1; ::_thesis: verum
end;
assume A4: ( cseq is 0 -convergent & cseq is non-zero ) ; ::_thesis: ( seq is 0 -convergent & seq is non-zero )
then A5: seq is non-zero by A1, Lm4;
(- **) (#) (** (#) seq) is convergent by A1, A4;
then ((- **) * **) (#) seq is convergent by CFUNCT_1:22;
then A6: seq is convergent by CFUNCT_1:26;
lim (** (#) seq) = 0 by A1, A4, CFDIFF_1:def_1;
then ** * (lim seq) = 0 by A6, COMSEQ_2:18;
hence ( seq is 0 -convergent & seq is non-zero ) by A6, A5, CFDIFF_1:def_1; ::_thesis: verum
end;
theorem Th2: :: CFDIFF_2:2
for f being PartFunc of COMPLEX,COMPLEX
for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) ) & ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) ) & z0 = x0 + (y0 * **) & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) )
proof
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) ) & ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) ) & z0 = x0 + (y0 * **) & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) )
let u, v be PartFunc of (REAL 2),REAL; ::_thesis: for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) ) & ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) ) & z0 = x0 + (y0 * **) & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) )
let z0 be Complex; ::_thesis: for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) ) & ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) ) & z0 = x0 + (y0 * **) & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) )
let x0, y0 be Real; ::_thesis: for xy0 being Element of REAL 2 st ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) ) & ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) ) & z0 = x0 + (y0 * **) & xy0 = <*x0,y0*> & f is_differentiable_in z0 holds
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) )
let xy0 be Element of REAL 2; ::_thesis: ( ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) ) & ( for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) ) & z0 = x0 + (y0 * **) & xy0 = <*x0,y0*> & f is_differentiable_in z0 implies ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) ) )
assume that
A1: for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * **)) ) and
A2: for x, y being Real st x + (y * **) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * **)) ) and
A3: z0 = x0 + (y0 * **) and
A4: xy0 = <*x0,y0*> and
A5: f is_differentiable_in z0 ; ::_thesis: ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) )
deffunc H1( Real) -> Element of REAL = (Im (diff (f,z0))) * $1;
consider LD2 being Function of REAL,REAL such that
A6: for x being Real holds LD2 . x = H1(x) from FUNCT_2:sch_4();
reconsider LD2 = LD2 as LinearFunc by A6, FDIFF_1:def_3;
deffunc H2( Real) -> Element of REAL = (Re (diff (f,z0))) * $1;
consider LD1 being Function of REAL,REAL such that
A7: for x being Real holds LD1 . x = H2(x) from FUNCT_2:sch_4();
A8: for y being Real holds (v * (reproj (2,xy0))) . y = v . <*x0,y*>
proof
let y be Real; ::_thesis: (v * (reproj (2,xy0))) . y = v . <*x0,y*>
y in REAL ;
then y in dom (reproj (2,xy0)) by PDIFF_1:def_5;
hence (v * (reproj (2,xy0))) . y = v . ((reproj (2,xy0)) . y) by FUNCT_1:13
.= v . (Replace (xy0,2,y)) by PDIFF_1:def_5
.= v . <*x0,y*> by A4, FINSEQ_7:14 ;
::_thesis: verum
end;
A9: for y being Real holds (u * (reproj (2,xy0))) . y = u . <*x0,y*>
proof
let y be Real; ::_thesis: (u * (reproj (2,xy0))) . y = u . <*x0,y*>
y in REAL ;
then y in dom (reproj (2,xy0)) by PDIFF_1:def_5;
hence (u * (reproj (2,xy0))) . y = u . ((reproj (2,xy0)) . y) by FUNCT_1:13
.= u . (Replace (xy0,2,y)) by PDIFF_1:def_5
.= u . <*x0,y*> by A4, FINSEQ_7:14 ;
::_thesis: verum
end;
A10: (proj (2,2)) . xy0 = xy0 . 2 by PDIFF_1:def_1
.= y0 by A4, FINSEQ_1:44 ;
reconsider LD1 = LD1 as LinearFunc by A7, FDIFF_1:def_3;
deffunc H3( Real) -> Element of REAL = - ((Im (diff (f,z0))) * $1);
consider LD3 being Function of REAL,REAL such that
A11: for x being Real holds LD3 . x = H3(x) from FUNCT_2:sch_4();
for x being Real holds LD3 . x = (- (Im (diff (f,z0)))) * x
proof
let x be Real; ::_thesis: LD3 . x = (- (Im (diff (f,z0)))) * x
thus LD3 . x = - ((Im (diff (f,z0))) * x) by A11
.= (- (Im (diff (f,z0)))) * x ; ::_thesis: verum
end;
then reconsider LD3 = LD3 as LinearFunc by FDIFF_1:def_3;
reconsider z0 = z0 as Element of COMPLEX by XCMPLX_0:def_2;
consider N being Neighbourhood of z0 such that
A12: N c= dom f and
A13: ex L being C_LinearFunc ex R being C_RestFunc st
( diff (f,z0) = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A5, CFDIFF_1:def_7;
consider L being C_LinearFunc, R being C_RestFunc such that
A14: ( diff (f,z0) = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A13;
deffunc H4( Real) -> Element of REAL = (Im R) . ($1 * **);
consider R4 being Function of REAL,REAL such that
A15: for y being Real holds R4 . y = H4(y) from FUNCT_2:sch_4();
A16: for z being Complex st z in N holds
(f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0))
proof
let z be Complex; ::_thesis: ( z in N implies (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0)) )
assume A17: z in N ; ::_thesis: (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0))
reconsider z = z as Element of COMPLEX by XCMPLX_0:def_2;
consider a0 being Element of COMPLEX such that
A18: for w being Element of COMPLEX holds L /. w = a0 * w by CFDIFF_1:def_4;
L /. (1r * (z - z0)) = (a0 * 1r) * (z - z0) by A18
.= (L /. 1r) * (z - z0) by A18 ;
hence (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0)) by A14, A17; ::_thesis: verum
end;
A19: for x, y being Real st x + (y * **) in N & x0 + (y0 * **) in N holds
(f . (x + (y * **))) - (f . (x0 + (y0 * **))) = ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) + (R /. ((x + (y * **)) - (x0 + (y0 * **))))
proof
let x, y be Real; ::_thesis: ( x + (y * **) in N & x0 + (y0 * **) in N implies (f . (x + (y * **))) - (f . (x0 + (y0 * **))) = ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) + (R /. ((x + (y * **)) - (x0 + (y0 * **)))) )
assume A20: ( x + (y * **) in N & x0 + (y0 * **) in N ) ; ::_thesis: (f . (x + (y * **))) - (f . (x0 + (y0 * **))) = ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) + (R /. ((x + (y * **)) - (x0 + (y0 * **))))
then ( f . (x + (y * **)) = f /. (x + (y * **)) & f . (x0 + (y0 * **)) = f /. (x0 + (y0 * **)) ) by A12, PARTFUN1:def_6;
hence (f . (x + (y * **))) - (f . (x0 + (y0 * **))) = ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) + (R /. ((x + (y * **)) - (x0 + (y0 * **)))) by A16, A20, A3; ::_thesis: verum
end;
A21: dom R = COMPLEX by PARTFUN1:def_2;
for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 )
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz0 = h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 = hz0 as non-zero 0 -convergent Complex_Sequence by Lm3;
set hz = ** (#) hz0;
reconsider hz = ** (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_")_(#)_(R4_/*_h))_._n_=_Re_(((hz_")_(#)_(R_/*_hz))_._n)
A22: rng hz c= dom R by A21;
dom R4 = REAL by PARTFUN1:def_2;
then A23: rng h c= dom R4 ;
let n be Element of NAT ; ::_thesis: ((h ") (#) (R4 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)
A24: ( Im ((h . n) ") = 0 & Re ((h . n) ") = (h . n) " ) by COMPLEX1:def_1, COMPLEX1:def_2;
A25: hz . n = (h . n) * ** by VALUED_1:6;
(h . n) * ** in COMPLEX ;
then A26: (h . n) * ** in dom (Im R) by Th1;
thus ((h ") (#) (R4 /* h)) . n = ((h ") . n) * ((R4 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R4 /* h) . n) by VALUED_1:10
.= ((h . n) ") * (R4 . (h . n)) by A23, FUNCT_2:108
.= ((h . n) ") * ((Im R) . ((h . n) * **)) by A15
.= ((Re ((h . n) ")) * (Im (R . ((h . n) * **)))) + ((Re (R . ((h . n) * **))) * (Im ((h . n) "))) by A26, A24, COMSEQ_3:def_4
.= Im ((((hz . n) / **) ") * (R . (hz . n))) by A25, COMPLEX1:9
.= Im ((** / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213
.= Im ((** * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10
.= Im (** * (((hz ") . n) * (R . (hz . n))))
.= ((Re **) * (Im (((hz ") . n) * (R /. (hz . n))))) + ((Re (((hz ") . n) * (R /. (hz . n)))) * (Im **)) by COMPLEX1:9
.= Re (((hz ") . n) * ((R /* hz) . n)) by A22, COMPLEX1:7, FUNCT_2:109
.= Re (((hz ") (#) (R /* hz)) . n) by VALUED_1:5 ; ::_thesis: verum
end;
then A27: (h ") (#) (R4 /* h) = Re ((hz ") (#) (R /* hz)) by COMSEQ_3:def_5;
( (hz ") (#) (R /* hz) is convergent & lim ((hz ") (#) (R /* hz)) = 0 ) by CFDIFF_1:def_3;
hence ( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 ) by A27, COMPLEX1:4, COMSEQ_3:41; ::_thesis: verum
end;
then reconsider R4 = R4 as RestFunc by FDIFF_1:def_2;
deffunc H5( Real) -> Element of REAL = (Re R) . ($1 * **);
A28: dom R = COMPLEX by PARTFUN1:def_2;
consider R2 being Function of REAL,REAL such that
A29: for y being Real holds R2 . y = H5(y) from FUNCT_2:sch_4();
for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R2 /* h) is convergent & lim ((h ") (#) (R2 /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R2 /* h) is convergent & lim ((h ") (#) (R2 /* h)) = 0 )
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz0 = h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 = hz0 as non-zero 0 -convergent Complex_Sequence by Lm3;
set hz = ** (#) hz0;
reconsider hz = ** (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;
A30: (hz ") (#) (R /* hz) is convergent by CFDIFF_1:def_3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_")_(#)_(R2_/*_h))_._n_=_-_((Im_((hz_")_(#)_(R_/*_hz)))_._n)
dom R = COMPLEX by PARTFUN1:def_2;
then A31: rng hz c= dom R ;
dom R2 = REAL by PARTFUN1:def_2;
then A32: rng h c= dom R2 ;
let n be Element of NAT ; ::_thesis: ((h ") (#) (R2 /* h)) . n = - ((Im ((hz ") (#) (R /* hz))) . n)
A33: ( Im ((h . n) ") = 0 & Re ((h . n) ") = (h . n) " ) by COMPLEX1:def_1, COMPLEX1:def_2;
A34: hz . n = (h . n) * ** by VALUED_1:6;
dom (Re R) = COMPLEX by Th1;
then A35: (h . n) * ** in dom (Re R) ;
A36: R . (hz . n) = R /. (hz . n) ;
thus ((h ") (#) (R2 /* h)) . n = ((h ") . n) * ((R2 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R2 /* h) . n) by VALUED_1:10
.= ((h . n) ") * (R2 . (h . n)) by A32, FUNCT_2:108
.= ((h . n) ") * ((Re R) . ((h . n) * **)) by A29
.= ((Re ((h . n) ")) * (Re (R . ((h . n) * **)))) - ((Im ((h . n) ")) * (Im (R . ((h . n) * **)))) by A35, A33, COMSEQ_3:def_3
.= Re ((((hz . n) / **) ") * (R . (hz . n))) by A34, COMPLEX1:9
.= Re ((** / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213
.= Re ((** * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10
.= Re (** * (((hz ") . n) * (R . (hz . n))))
.= ((Re **) * (Re (((hz ") . n) * (R . (hz . n))))) - ((Im **) * (Im (((hz ") . n) * (R . (hz . n))))) by COMPLEX1:9
.= - (Im (((hz ") . n) * ((R /* hz) . n))) by A36, A31, COMPLEX1:7, FUNCT_2:109
.= - (Im (((hz ") (#) (R /* hz)) . n)) by VALUED_1:5
.= - ((Im ((hz ") (#) (R /* hz))) . n) by COMSEQ_3:def_6 ; ::_thesis: verum
end;
then A37: (h ") (#) (R2 /* h) = - (Im ((hz ") (#) (R /* hz))) by SEQ_1:10;
lim ((hz ") (#) (R /* hz)) = 0 by CFDIFF_1:def_3;
then lim (Im ((hz ") (#) (R /* hz))) = Im 0 by A30, COMSEQ_3:41;
then lim ((h ") (#) (R2 /* h)) = - (Im 0) by A37, A30, SEQ_2:10
.= 0 by COMPLEX1:4 ;
hence ( (h ") (#) (R2 /* h) is convergent & lim ((h ") (#) (R2 /* h)) = 0 ) by A37, A30, SEQ_2:9; ::_thesis: verum
end;
then reconsider R2 = R2 as RestFunc by FDIFF_1:def_2;
consider r0 being Real such that
A38: 0 < r0 and
A39: { y where y is Complex : |.(y - z0).| < r0 } c= N by CFDIFF_1:def_5;
set Ny0 = ].(y0 - r0),(y0 + r0).[;
reconsider Ny0 = ].(y0 - r0),(y0 + r0).[ as Neighbourhood of y0 by A38, RCOMP_1:def_6;
A40: for y being Real st y in Ny0 holds
x0 + (y * **) in N
proof
let y be Real; ::_thesis: ( y in Ny0 implies x0 + (y * **) in N )
|.((x0 + (y * **)) - z0).| = |.((y - y0) * **).| by A3;
then A41: |.((x0 + (y * **)) - z0).| = |.(y - y0).| * |.**.| by COMPLEX1:65;
assume y in Ny0 ; ::_thesis: x0 + (y * **) in N
then ( x0 + (y * **) is Complex & |.((x0 + (y * **)) - z0).| < r0 ) by A41, COMPLEX1:49, RCOMP_1:1;
then x0 + (y * **) in { w where w is Complex : |.(w - z0).| < r0 } ;
hence x0 + (y * **) in N by A39; ::_thesis: verum
end;
A42: for x, y being Real holds (diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **))) = (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * **)
proof
let x, y be Real; ::_thesis: (diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **))) = (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * **)
thus (diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **))) = ((Re (diff (f,z0))) + ((Im (diff (f,z0))) * **)) * ((x - x0) + ((y - y0) * **)) by COMPLEX1:13
.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * **) ; ::_thesis: verum
end;
A43: for x, y being Real holds Re ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) = ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))
proof
let x, y be Real; ::_thesis: Re ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) = ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))
thus Re ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) = Re ((((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * **)) by A42
.= ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0)) by COMPLEX1:12 ; ::_thesis: verum
end;
A44: for y being Real st y in Ny0 holds
(u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * **)))
proof
let y be Real; ::_thesis: ( y in Ny0 implies (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * **))) )
(x0 + (y * **)) - (x0 + (y0 * **)) in dom R by A28;
then A45: (y - y0) * ** in dom (Re R) by COMSEQ_3:def_3;
assume y in Ny0 ; ::_thesis: (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * **)))
then A46: x0 + (y * **) in N by A40;
then x0 + (y * **) in dom f by A12;
then A47: x0 + (y * **) in dom (Re f) by COMSEQ_3:def_3;
A48: x0 + (y0 * **) in N by A3, CFDIFF_1:7;
then x0 + (y0 * **) in dom f by A12;
then A49: x0 + (y0 * **) in dom (Re f) by COMSEQ_3:def_3;
(u . <*x0,y*>) - (u . <*x0,y0*>) = ((Re f) . (x0 + (y * **))) - (u . <*x0,y0*>) by A1, A12, A46
.= ((Re f) . (x0 + (y * **))) - ((Re f) . (x0 + (y0 * **))) by A1, A12, A48
.= (Re (f . (x0 + (y * **)))) - ((Re f) . (x0 + (y0 * **))) by A47, COMSEQ_3:def_3
.= (Re (f . (x0 + (y * **)))) - (Re (f . (x0 + (y0 * **)))) by A49, COMSEQ_3:def_3
.= Re ((f . (x0 + (y * **))) - (f . (x0 + (y0 * **)))) by COMPLEX1:19
.= Re (((diff (f,z0)) * ((x0 + (y * **)) - (x0 + (y0 * **)))) + (R /. ((x0 + (y * **)) - (x0 + (y0 * **))))) by A19, A46, A48
.= (Re ((diff (f,z0)) * ((x0 + (y * **)) - (x0 + (y0 * **))))) + (Re (R /. ((x0 + (y * **)) - (x0 + (y0 * **))))) by COMPLEX1:8
.= (((Re (diff (f,z0))) * (x0 - x0)) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * **)) - (x0 + (y0 * **))))) by A43
.= (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * **))) by A45, COMSEQ_3:def_3 ;
hence (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * **))) ; ::_thesis: verum
end;
A50: for y being Real st y in Ny0 holds
((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))
proof
let y be Real; ::_thesis: ( y in Ny0 implies ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0)) )
assume A51: y in Ny0 ; ::_thesis: ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))
thus ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (u . <*x0,y*>) - ((u * (reproj (2,xy0))) . y0) by A9
.= (u . <*x0,y*>) - (u . <*x0,y0*>) by A9
.= (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * **))) by A44, A51
.= (LD3 . (y - y0)) + ((Re R) . ((x0 - x0) + ((y - y0) * **))) by A11
.= (LD3 . (y - y0)) + (R2 . (y - y0)) by A29 ; ::_thesis: verum
end;
A52: for x, y being Real holds Im ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) = ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))
proof
let x, y be Real; ::_thesis: Im ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) = ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))
thus Im ((diff (f,z0)) * ((x + (y * **)) - (x0 + (y0 * **)))) = Im ((((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * **)) by A42
.= ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0)) by COMPLEX1:12 ; ::_thesis: verum
end;
A53: for y being Real st y in Ny0 holds
(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **)))
proof
let y be Real; ::_thesis: ( y in Ny0 implies (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **))) )
(x0 + (y * **)) - (x0 + (y0 * **)) in dom R by A28;
then A54: (y - y0) * ** in dom (Im R) by COMSEQ_3:def_4;
assume y in Ny0 ; ::_thesis: (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **)))
then A55: x0 + (y * **) in N by A40;
then x0 + (y * **) in dom f by A12;
then A56: x0 + (y * **) in dom (Im f) by COMSEQ_3:def_4;
A57: x0 + (y0 * **) in N by A3, CFDIFF_1:7;
then x0 + (y0 * **) in dom f by A12;
then A58: x0 + (y0 * **) in dom (Im f) by COMSEQ_3:def_4;
(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Im f) . (x0 + (y * **))) - (v . <*x0,y0*>) by A2, A12, A55
.= ((Im f) . (x0 + (y * **))) - ((Im f) . (x0 + (y0 * **))) by A2, A12, A57
.= (Im (f . (x0 + (y * **)))) - ((Im f) . (x0 + (y0 * **))) by A56, COMSEQ_3:def_4
.= (Im (f . (x0 + (y * **)))) - (Im (f . (x0 + (y0 * **)))) by A58, COMSEQ_3:def_4
.= Im ((f . (x0 + (y * **))) - (f . (x0 + (y0 * **)))) by COMPLEX1:19
.= Im (((diff (f,z0)) * ((x0 + (y * **)) - (x0 + (y0 * **)))) + (R /. ((x0 + (y * **)) - (x0 + (y0 * **))))) by A19, A55, A57
.= (Im ((diff (f,z0)) * ((x0 + (y * **)) - (x0 + (y0 * **))))) + (Im (R /. ((x0 + (y * **)) - (x0 + (y0 * **))))) by COMPLEX1:8
.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R /. ((x0 + (y * **)) - (x0 + (y0 * **))))) by A52
.= ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **))) by A54, COMSEQ_3:def_4 ;
hence (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **))) ; ::_thesis: verum
end;
A59: for y being Real st y in Ny0 holds
((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))
proof
let y be Real; ::_thesis: ( y in Ny0 implies ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0)) )
assume A60: y in Ny0 ; ::_thesis: ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))
thus ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (v . <*x0,y*>) - ((v * (reproj (2,xy0))) . y0) by A8
.= (v . <*x0,y*>) - (v . <*x0,y0*>) by A8
.= ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **))) by A53, A60
.= (LD1 . (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * **))) by A7
.= (LD1 . (y - y0)) + (R4 . (y - y0)) by A15 ; ::_thesis: verum
end;
now__::_thesis:_for_s_being_set_st_s_in_(reproj_(2,xy0))_.:_Ny0_holds_
s_in_dom_v
let s be set ; ::_thesis: ( s in (reproj (2,xy0)) .: Ny0 implies s in dom v )
assume s in (reproj (2,xy0)) .: Ny0 ; ::_thesis: s in dom v
then consider y being Element of REAL such that
A61: y in Ny0 and
A62: s = (reproj (2,xy0)) . y by FUNCT_2:65;
A63: x0 + (y * **) in N by A40, A61;
s = Replace (xy0,2,y) by A62, PDIFF_1:def_5
.= <*x0,y*> by A4, FINSEQ_7:14 ;
hence s in dom v by A2, A12, A63; ::_thesis: verum
end;
then ( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom v ) by FUNCT_2:def_1, TARSKI:def_3;
then A64: Ny0 c= dom (v * (reproj (2,xy0))) by FUNCT_3:3;
then A65: v * (reproj (2,xy0)) is_differentiable_in (proj (2,2)) . xy0 by A10, A59, FDIFF_1:def_4;
A66: for x being Real holds (v * (reproj (1,xy0))) . x = v . <*x,y0*>
proof
let x be Real; ::_thesis: (v * (reproj (1,xy0))) . x = v . <*x,y0*>
x in REAL ;
then x in dom (reproj (1,xy0)) by PDIFF_1:def_5;
hence (v * (reproj (1,xy0))) . x = v . ((reproj (1,xy0)) . x) by FUNCT_1:13
.= v . (Replace (xy0,1,x)) by PDIFF_1:def_5
.= v . <*x,y0*> by A4, FINSEQ_7:13 ;
::_thesis: verum
end;
now__::_thesis:_for_s_being_set_st_s_in_(reproj_(2,xy0))_.:_Ny0_holds_
s_in_dom_u
let s be set ; ::_thesis: ( s in (reproj (2,xy0)) .: Ny0 implies s in dom u )
assume s in (reproj (2,xy0)) .: Ny0 ; ::_thesis: s in dom u
then consider y being Element of REAL such that
A67: y in Ny0 and
A68: s = (reproj (2,xy0)) . y by FUNCT_2:65;
A69: x0 + (y * **) in N by A40, A67;
s = Replace (xy0,2,y) by A68, PDIFF_1:def_5
.= <*x0,y*> by A4, FINSEQ_7:14 ;
hence s in dom u by A1, A12, A69; ::_thesis: verum
end;
then ( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom u ) by FUNCT_2:def_1, TARSKI:def_3;
then A70: Ny0 c= dom (u * (reproj (2,xy0))) by FUNCT_3:3;
then A71: u * (reproj (2,xy0)) is_differentiable_in (proj (2,2)) . xy0 by A10, A50, FDIFF_1:def_4;
LD3 . 1 = - ((Im (diff (f,z0))) * 1) by A11
.= - (Im (diff (f,z0))) ;
then A72: partdiff (u,xy0,2) = - (Im (diff (f,z0))) by A10, A50, A70, A71, FDIFF_1:def_5;
A73: LD1 . 1 = (Re (diff (f,z0))) * 1 by A7
.= Re (diff (f,z0)) ;
A74: (proj (1,2)) . xy0 = xy0 . 1 by PDIFF_1:def_1
.= x0 by A4, FINSEQ_1:44 ;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by A38, RCOMP_1:def_6;
deffunc H6( Real) -> Element of REAL = (Im R) . $1;
consider R3 being Function of REAL,REAL such that
A75: for y being Real holds R3 . y = H6(y) from FUNCT_2:sch_4();
A76: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz = h as Complex_Sequence by FUNCT_2:6;
reconsider hz = hz as non-zero 0 -convergent Complex_Sequence by Lm3;
now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_")_(#)_(R3_/*_h))_._n_=_Im_(((hz_")_(#)_(R_/*_hz))_._n)
A77: dom R = COMPLEX by PARTFUN1:def_2;
then A78: rng hz c= dom R ;
let n be Element of NAT ; ::_thesis: ((h ") (#) (R3 /* h)) . n = Im (((hz ") (#) (R /* hz)) . n)
A79: ( Im ((h . n) ") = 0 & Re ((h . n) ") = (h . n) " ) by COMPLEX1:def_1, COMPLEX1:def_2;
A80: dom R3 = REAL by PARTFUN1:def_2;
then A81: rng h c= dom R3 ;
dom R3 c= dom (Im R) by A80, Th1, NUMBERS:11;
then A82: h . n in dom (Im R) by A80, TARSKI:def_3;
h . n in COMPLEX by XCMPLX_0:def_2;
then A83: R /. (h . n) = R . (h . n) by A77, PARTFUN1:def_6;
thus ((h ") (#) (R3 /* h)) . n = ((h ") . n) * ((R3 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R3 /* h) . n) by VALUED_1:10
.= ((h . n) ") * (R3 . (h . n)) by A81, FUNCT_2:108
.= ((h . n) ") * ((Im R) . (h . n)) by A75
.= ((Re ((h . n) ")) * (Im (R /. (h . n)))) + ((Re (R /. (h . n))) * (Im ((h . n) "))) by A83, A82, A79, COMSEQ_3:def_4
.= Im (((h . n) ") * (R /. (h . n))) by COMPLEX1:9
.= Im (((hz ") . n) * (R /. (hz . n))) by VALUED_1:10
.= Im (((hz ") . n) * ((R /* hz) . n)) by A78, FUNCT_2:109
.= Im (((hz ") (#) (R /* hz)) . n) by VALUED_1:5 ; ::_thesis: verum
end;
then A84: (h ") (#) (R3 /* h) = Im ((hz ") (#) (R /* hz)) by COMSEQ_3:def_6;
( (hz ") (#) (R /* hz) is convergent & lim ((hz ") (#) (R /* hz)) = 0 ) by CFDIFF_1:def_3;
hence ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 ) by A84, COMPLEX1:4, COMSEQ_3:41; ::_thesis: verum
end;
deffunc H7( Real) -> Element of REAL = (Re R) . $1;
consider R1 being Function of REAL,REAL such that
A85: for x being Real holds R1 . x = H7(x) from FUNCT_2:sch_4();
reconsider R3 = R3 as RestFunc by A76, FDIFF_1:def_2;
A86: for x being Real st x in Nx0 holds
x + (y0 * **) in N
proof
let x be Real; ::_thesis: ( x in Nx0 implies x + (y0 * **) in N )
assume x in Nx0 ; ::_thesis: x + (y0 * **) in N
then |.(x - x0).| < r0 by RCOMP_1:1;
then ( x + (y0 * **) is Complex & |.((x + (y0 * **)) - z0).| < r0 ) by A3;
then x + (y0 * **) in { y where y is Complex : |.(y - z0).| < r0 } ;
hence x + (y0 * **) in N by A39; ::_thesis: verum
end;
A87: for x being Real st x in Nx0 holds
(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * **)))
proof
let x be Real; ::_thesis: ( x in Nx0 implies (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * **))) )
(x + (y0 * **)) - (x0 + (y0 * **)) in dom R by A28;
then A88: x - x0 in dom (Im R) by COMSEQ_3:def_4;
assume x in Nx0 ; ::_thesis: (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * **)))
then A89: x + (y0 * **) in N by A86;
then x + (y0 * **) in dom f by A12;
then A90: x + (y0 * **) in dom (Im f) by COMSEQ_3:def_4;
A91: x0 + (y0 * **) in N by A3, CFDIFF_1:7;
then x0 + (y0 * **) in dom f by A12;
then A92: x0 + (y0 * **) in dom (Im f) by COMSEQ_3:def_4;
(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im f) . (x + (y0 * **))) - (v . <*x0,y0*>) by A2, A12, A89
.= ((Im f) . (x + (y0 * **))) - ((Im f) . (x0 + (y0 * **))) by A2, A12, A91
.= (Im (f . (x + (y0 * **)))) - ((Im f) . (x0 + (y0 * **))) by A90, COMSEQ_3:def_4
.= (Im (f . (x + (y0 * **)))) - (Im (f . (x0 + (y0 * **)))) by A92, COMSEQ_3:def_4
.= Im ((f . (x + (y0 * **))) - (f . (x0 + (y0 * **)))) by COMPLEX1:19
.= Im (((diff (f,z0)) * ((x + (y0 * **)) - (x0 + (y0 * **)))) + (R /. ((x + (y0 * *