:: 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 * )) - (x0 + (y0 * ))))) by A19, A89, A91 .= (Im ((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * ))))) + (Im (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by COMPLEX1:8 .= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A52 .= ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A88, COMSEQ_3:def_4 ; hence (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) ; ::_thesis: verum end; A93: for x being Real st x in Nx0 holds ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0)) proof let x be Real; ::_thesis: ( x in Nx0 implies ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0)) ) assume A94: x in Nx0 ; ::_thesis: ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0)) thus ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (v . <*x,y0*>) - ((v * (reproj (1,xy0))) . x0) by A66 .= (v . <*x,y0*>) - (v . <*x0,y0*>) by A66 .= ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A87, A94 .= (LD2 . (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A6 .= (LD2 . (x - x0)) + (R3 . (x - x0)) by A75 ; ::_thesis: verum end; for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* 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_")_(#)_(R1_/*_h))_._n_=_Re_(((hz_")_(#)_(R_/*_hz))_._n) dom R = COMPLEX by PARTFUN1:def_2; then A95: rng hz c= dom R ; let n be Element of NAT ; ::_thesis: ((h ") (#) (R1 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n) A96: ( Im ((h . n) ") = 0 & Re ((h . n) ") = (h . n) " ) by COMPLEX1:def_1, COMPLEX1:def_2; A97: dom R1 = REAL by PARTFUN1:def_2; then A98: rng h c= dom R1 ; dom R1 c= dom (Re R) by A97, Th1, NUMBERS:11; then A99: h . n in dom (Re R) by A97, TARSKI:def_3; thus ((h ") (#) (R1 /* h)) . n = ((h ") . n) * ((R1 /* h) . n) by SEQ_1:8 .= ((h . n) ") * ((R1 /* h) . n) by VALUED_1:10 .= ((h . n) ") * (R1 /. (h . n)) by A98, FUNCT_2:109 .= ((h . n) ") * ((Re R) . (h . n)) by A85 .= ((Re ((h . n) ")) * (Re (R . (h . n)))) - ((Im ((h . n) ")) * (Im (R . (h . n)))) by A99, A96, COMSEQ_3:def_3 .= Re (((h . n) ") * (R . (h . n))) by COMPLEX1:9 .= Re (((hz ") . n) * (R /. (hz . n))) by VALUED_1:10 .= Re (((hz ") . n) * ((R /* hz) . n)) by A95, FUNCT_2:109 .= Re (((hz ") (#) (R /* hz)) . n) by VALUED_1:5 ; ::_thesis: verum end; then A100: (h ") (#) (R1 /* 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 ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by A100, COMPLEX1:4, COMSEQ_3:41; ::_thesis: verum end; then reconsider R1 = R1 as RestFunc by FDIFF_1:def_2; A101: LD2 . 1 = (Im (diff (f,z0))) * 1 by A6 .= Im (diff (f,z0)) ; A102: for x being Real holds (u * (reproj (1,xy0))) . x = u . <*x,y0*> proof let x be Real; ::_thesis: (u * (reproj (1,xy0))) . x = u . <*x,y0*> x in REAL ; then x in dom (reproj (1,xy0)) by PDIFF_1:def_5; hence (u * (reproj (1,xy0))) . x = u . ((reproj (1,xy0)) . x) by FUNCT_1:13 .= u . (Replace (xy0,1,x)) by PDIFF_1:def_5 .= u . <*x,y0*> by A4, FINSEQ_7:13 ; ::_thesis: verum end; A103: for x being Real st x in Nx0 holds (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) proof let x be Real; ::_thesis: ( x in Nx0 implies (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) ) (x + (y0 * )) - (x0 + (y0 * )) in dom R by A28; then A104: x - x0 in dom (Re R) by COMSEQ_3:def_3; assume x in Nx0 ; ::_thesis: (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) then A105: x + (y0 * ) in N by A86; then x + (y0 * ) in dom f by A12; then A106: x + (y0 * ) in dom (Re f) by COMSEQ_3:def_3; A107: x0 + (y0 * ) in N by A3, CFDIFF_1:7; then x0 + (y0 * ) in dom f by A12; then A108: x0 + (y0 * ) in dom (Re f) by COMSEQ_3:def_3; (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re f) . (x + (y0 * ))) - (u . <*x0,y0*>) by A1, A12, A105 .= ((Re f) . (x + (y0 * ))) - ((Re f) . (x0 + (y0 * ))) by A1, A12, A107 .= (Re (f . (x + (y0 * )))) - ((Re f) . (x0 + (y0 * ))) by A106, COMSEQ_3:def_3 .= (Re (f . (x + (y0 * )))) - (Re (f . (x0 + (y0 * )))) by A108, COMSEQ_3:def_3 .= Re ((f . (x + (y0 * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:19 .= Re (((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * )))) + (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A19, A105, A107 .= (Re ((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * ))))) + (Re (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by COMPLEX1:8 .= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A43 .= ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A104, COMSEQ_3:def_3 ; hence (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) ; ::_thesis: verum end; A109: for x being Real st x in Nx0 holds ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) proof let x be Real; ::_thesis: ( x in Nx0 implies ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) ) assume A110: x in Nx0 ; ::_thesis: ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) thus ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (u . <*x,y0*>) - ((u * (reproj (1,xy0))) . x0) by A102 .= (u . <*x,y0*>) - (u . <*x0,y0*>) by A102 .= ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A103, A110 .= (LD1 . (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A7 .= (LD1 . (x - x0)) + (R1 . (x - x0)) by A85 ; ::_thesis: verum end; now__::_thesis:_for_s_being_set_st_s_in_(reproj_(1,xy0))_.:_Nx0_holds_ s_in_dom_v let s be set ; ::_thesis: ( s in (reproj (1,xy0)) .: Nx0 implies s in dom v ) assume s in (reproj (1,xy0)) .: Nx0 ; ::_thesis: s in dom v then consider x being Element of REAL such that A111: x in Nx0 and A112: s = (reproj (1,xy0)) . x by FUNCT_2:65; A113: x + (y0 * ) in N by A86, A111; s = Replace (xy0,1,x) by A112, PDIFF_1:def_5 .= <*x,y0*> by A4, FINSEQ_7:13 ; hence s in dom v by A2, A12, A113; ::_thesis: verum end; then ( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom v ) by FUNCT_2:def_1, TARSKI:def_3; then A114: Nx0 c= dom (v * (reproj (1,xy0))) by FUNCT_3:3; then A115: v * (reproj (1,xy0)) is_differentiable_in (proj (1,2)) . xy0 by A74, A93, FDIFF_1:def_4; now__::_thesis:_for_s_being_set_st_s_in_(reproj_(1,xy0))_.:_Nx0_holds_ s_in_dom_u let s be set ; ::_thesis: ( s in (reproj (1,xy0)) .: Nx0 implies s in dom u ) assume s in (reproj (1,xy0)) .: Nx0 ; ::_thesis: s in dom u then consider x being Element of REAL such that A116: x in Nx0 and A117: s = (reproj (1,xy0)) . x by FUNCT_2:65; A118: x + (y0 * ) in N by A86, A116; s = Replace (xy0,1,x) by A117, PDIFF_1:def_5 .= <*x,y0*> by A4, FINSEQ_7:13 ; hence s in dom u by A1, A12, A118; ::_thesis: verum end; then ( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom u ) by FUNCT_2:def_1, TARSKI:def_3; then A119: Nx0 c= dom (u * (reproj (1,xy0))) by FUNCT_3:3; then u * (reproj (1,xy0)) is_differentiable_in (proj (1,2)) . xy0 by A74, A109, FDIFF_1:def_4; hence ( 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) ) by A74, A10, A109, A93, A59, A119, A71, A72, A101, A114, A115, A73, A64, A65, FDIFF_1:def_5, PDIFF_1:def_11; ::_thesis: verum end; Lm6: for x, y being Real for vx, vy being Point of (REAL-NS 1) st vx = <*x*> & vy = <*y*> holds ( vx + vy = <*(x + y)*> & vx - vy = <*(x - y)*> ) proof let x, y be Real; ::_thesis: for vx, vy being Point of (REAL-NS 1) st vx = <*x*> & vy = <*y*> holds ( vx + vy = <*(x + y)*> & vx - vy = <*(x - y)*> ) let vx, vy be Point of (REAL-NS 1); ::_thesis: ( vx = <*x*> & vy = <*y*> implies ( vx + vy = <*(x + y)*> & vx - vy = <*(x - y)*> ) ) assume A1: ( vx = <*x*> & vy = <*y*> ) ; ::_thesis: ( vx + vy = <*(x + y)*> & vx - vy = <*(x - y)*> ) reconsider vx1 = vx, vy1 = vy as Element of REAL 1 by REAL_NS1:def_4; thus vx + vy = vx1 + vy1 by REAL_NS1:2 .= <*(x + y)*> by A1, RVSUM_1:13 ; ::_thesis: vx - vy = <*(x - y)*> thus vx - vy = vx1 - vy1 by REAL_NS1:5 .= <*(x - y)*> by A1, RVSUM_1:29 ; ::_thesis: verum end; Lm7: for x, y, z, w being Real for vx, vy being Element of REAL 2 st vx = <*x,y*> & vy = <*z,w*> holds ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) proof let x, y, z, w be Real; ::_thesis: for vx, vy being Element of REAL 2 st vx = <*x,y*> & vy = <*z,w*> holds ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) let vx, vy be Element of REAL 2; ::_thesis: ( vx = <*x,y*> & vy = <*z,w*> implies ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) ) reconsider x1 = x, y1 = y, z1 = z, w1 = w as Element of REAL ; assume A1: ( vx = <*x,y*> & vy = <*z,w*> ) ; ::_thesis: ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) hence vx + vy = <*(addreal . (x1,z1)),(addreal . (y1,w1))*> by FINSEQ_2:75 .= <*(x1 + z1),(addreal . (y1,w1))*> by BINOP_2:def_9 .= <*(x + z),(y + w)*> by BINOP_2:def_9 ; ::_thesis: vx - vy = <*(x - z),(y - w)*> thus vx - vy = <*(diffreal . (x1,z1)),(diffreal . (y1,w1))*> by A1, FINSEQ_2:75 .= <*(x1 - z1),(diffreal . (y1,w1))*> by BINOP_2:def_10 .= <*(x - z),(y - w)*> by BINOP_2:def_10 ; ::_thesis: verum end; Lm8: for x, y, a being Real for vx being Element of REAL 2 st vx = <*x,y*> holds a * vx = <*(a * x),(a * y)*> proof let x, y, a be Real; ::_thesis: for vx being Element of REAL 2 st vx = <*x,y*> holds a * vx = <*(a * x),(a * y)*> let vx be Element of REAL 2; ::_thesis: ( vx = <*x,y*> implies a * vx = <*(a * x),(a * y)*> ) reconsider x1 = x, y1 = y as Element of REAL ; assume vx = <*x,y*> ; ::_thesis: a * vx = <*(a * x),(a * y)*> hence a * vx = <*((a multreal) . x1),((a multreal) . y1)*> by FINSEQ_2:36 .= <*(a * x1),((a multreal) . y1)*> by RVSUM_1:5 .= <*(a * x),(a * y)*> by RVSUM_1:5 ; ::_thesis: verum end; Lm9: for x, y being Real holds <*x,y*> is Point of (REAL-NS 2) proof let x, y be Real; ::_thesis: <*x,y*> is Point of (REAL-NS 2) reconsider x1 = x, y1 = y as Element of REAL ; <*x1,y1*> in REAL 2 by FINSEQ_2:101; hence <*x,y*> is Point of (REAL-NS 2) by REAL_NS1:def_4; ::_thesis: verum end; Lm10: for x, y, z, w being Real for vx, vy being Point of (REAL-NS 2) st vx = <*x,y*> & vy = <*z,w*> holds ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) proof let x, y, z, w be Real; ::_thesis: for vx, vy being Point of (REAL-NS 2) st vx = <*x,y*> & vy = <*z,w*> holds ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) let vx, vy be Point of (REAL-NS 2); ::_thesis: ( vx = <*x,y*> & vy = <*z,w*> implies ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) ) assume A1: ( vx = <*x,y*> & vy = <*z,w*> ) ; ::_thesis: ( vx + vy = <*(x + z),(y + w)*> & vx - vy = <*(x - z),(y - w)*> ) reconsider vx1 = vx, vy1 = vy as Element of REAL 2 by REAL_NS1:def_4; thus vx + vy = vx1 + vy1 by REAL_NS1:2 .= <*(x + z),(y + w)*> by A1, Lm7 ; ::_thesis: vx - vy = <*(x - z),(y - w)*> thus vx - vy = vx1 - vy1 by REAL_NS1:5 .= <*(x - z),(y - w)*> by A1, Lm7 ; ::_thesis: verum end; Lm11: for x, y, a being Real for vx being Point of (REAL-NS 2) st vx = <*x,y*> holds a * vx = <*(a * x),(a * y)*> proof let x, y, a be Real; ::_thesis: for vx being Point of (REAL-NS 2) st vx = <*x,y*> holds a * vx = <*(a * x),(a * y)*> let vx be Point of (REAL-NS 2); ::_thesis: ( vx = <*x,y*> implies a * vx = <*(a * x),(a * y)*> ) assume A1: vx = <*x,y*> ; ::_thesis: a * vx = <*(a * x),(a * y)*> reconsider vx1 = vx as Element of REAL 2 by REAL_NS1:def_4; thus a * vx = a * vx1 by REAL_NS1:3 .= <*(a * x),(a * y)*> by A1, Lm8 ; ::_thesis: verum end; Lm12: for u being PartFunc of (REAL 2),REAL for xy being Element of REAL 2 st xy in dom u holds (<>* u) . xy = <*(u . xy)*> proof let u be PartFunc of (REAL 2),REAL; ::_thesis: for xy being Element of REAL 2 st xy in dom u holds (<>* u) . xy = <*(u . xy)*> let xy be Element of REAL 2; ::_thesis: ( xy in dom u implies (<>* u) . xy = <*(u . xy)*> ) assume xy in dom u ; ::_thesis: (<>* u) . xy = <*(u . xy)*> hence (<>* u) . xy = ((proj (1,1)) ") . (u . xy) by FUNCT_1:13 .= <*(u . xy)*> by PDIFF_1:1 ; ::_thesis: verum end; Lm13: for u being PartFunc of (REAL 2),REAL for x, y being Real st <*x,y*> in dom u holds (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*> proof set W = (proj (1,1)) " ; let u be PartFunc of (REAL 2),REAL; ::_thesis: for x, y being Real st <*x,y*> in dom u holds (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*> let x, y be Real; ::_thesis: ( <*x,y*> in dom u implies (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*> ) assume A1: <*x,y*> in dom u ; ::_thesis: (<>* u) /. <*x,y*> = <*(u /. <*x,y*>)*> rng u c= dom ((proj (1,1)) ") by PDIFF_1:2; then dom (<>* u) = dom u by RELAT_1:27; hence (<>* u) /. <*x,y*> = (<>* u) . <*x,y*> by A1, PARTFUN1:def_6 .= ((proj (1,1)) ") . (u . <*x,y*>) by A1, FUNCT_1:13 .= <*(u . <*x,y*>)*> by PDIFF_1:1 .= <*(u /. <*x,y*>)*> by A1, PARTFUN1:def_6 ; ::_thesis: verum end; Lm14: for x, y being Real for z being Complex for v being Element of (REAL-NS 2) st z = x + (y * ) & v = <*x,y*> holds |.z.| = ||.v.|| proof let x, y be Real; ::_thesis: for z being Complex for v being Element of (REAL-NS 2) st z = x + (y * ) & v = <*x,y*> holds |.z.| = ||.v.|| let z be Complex; ::_thesis: for v being Element of (REAL-NS 2) st z = x + (y * ) & v = <*x,y*> holds |.z.| = ||.v.|| let v be Element of (REAL-NS 2); ::_thesis: ( z = x + (y * ) & v = <*x,y*> implies |.z.| = ||.v.|| ) assume that A1: z = x + (y * ) and A2: v = <*x,y*> ; ::_thesis: |.z.| = ||.v.|| A3: Im z = y by A1, COMPLEX1:12; reconsider xx = <*x,y*> as Element of REAL 2 by FINSEQ_2:101; A4: ( |.xx.| = ||.v.|| & Re z = x ) by A1, A2, COMPLEX1:12, REAL_NS1:1; reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22; xx1 `2 = y by FINSEQ_1:44; then A5: (sqr xx) . 2 = y ^2 by VALUED_1:11; xx1 `1 = x by FINSEQ_1:44; then ( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 ) by CARD_1:def_7, VALUED_1:11; then sqr xx = <*(x ^2),(y ^2)*> by A5, FINSEQ_1:44; hence |.z.| = ||.v.|| by A4, A3, RVSUM_1:77; ::_thesis: verum end; Lm15: for x, y being Real for z being Complex st z = x + (y * ) holds |.z.| <= (abs x) + (abs y) proof let x, y be Real; ::_thesis: for z being Complex st z = x + (y * ) holds |.z.| <= (abs x) + (abs y) let z be Complex; ::_thesis: ( z = x + (y * ) implies |.z.| <= (abs x) + (abs y) ) assume z = x + (y * ) ; ::_thesis: |.z.| <= (abs x) + (abs y) then ( Re z = x & Im z = y ) by COMPLEX1:12; hence |.z.| <= (abs x) + (abs y) by COMPLEX1:78; ::_thesis: verum end; Lm16: for x, y being Real holds ( abs x <= |.(x + (y * )).| & abs y <= |.(x + (y * )).| ) proof let x, y be Real; ::_thesis: ( abs x <= |.(x + (y * )).| & abs y <= |.(x + (y * )).| ) set z = x + (y * ); ( Re (x + (y * )) = x & Im (x + (y * )) = y ) by COMPLEX1:12; hence ( abs x <= |.(x + (y * )).| & abs y <= |.(x + (y * )).| ) by COMPLEX1:79; ::_thesis: verum end; Lm17: for x, y being Real for v being Element of (REAL-NS 2) st v = <*x,y*> holds ||.v.|| <= (abs x) + (abs y) proof let x, y be Real; ::_thesis: for v being Element of (REAL-NS 2) st v = <*x,y*> holds ||.v.|| <= (abs x) + (abs y) let v be Element of (REAL-NS 2); ::_thesis: ( v = <*x,y*> implies ||.v.|| <= (abs x) + (abs y) ) reconsider z = x + (y * ) as Complex ; assume v = <*x,y*> ; ::_thesis: ||.v.|| <= (abs x) + (abs y) then |.z.| = ||.v.|| by Lm14; hence ||.v.|| <= (abs x) + (abs y) by Lm15; ::_thesis: verum end; theorem Th3: :: CFDIFF_2:3 for seq being Real_Sequence holds ( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) ) proof let seq be Real_Sequence; ::_thesis: ( seq is convergent & lim seq = 0 iff ( abs seq is convergent & lim (abs seq) = 0 ) ) thus ( seq is convergent & lim seq = 0 implies ( abs seq is convergent & lim (abs seq) = 0 ) ) ::_thesis: ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) ) proof assume that A1: seq is convergent and A2: lim seq = 0 ; ::_thesis: ( abs seq is convergent & lim (abs seq) = 0 ) lim (abs seq) = abs 0 by A1, A2, SEQ_4:14 .= 0 by ABSVALUE:2 ; hence ( abs seq is convergent & lim (abs seq) = 0 ) by A1; ::_thesis: verum end; thus ( abs seq is convergent & lim (abs seq) = 0 implies ( seq is convergent & lim seq = 0 ) ) by SEQ_4:15; ::_thesis: verum end; theorem Th4: :: CFDIFF_2:4 for X being RealNormSpace for seq being sequence of X holds ( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ) proof let X be RealNormSpace; ::_thesis: for seq being sequence of X holds ( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ) let seq be sequence of X; ::_thesis: ( seq is convergent & lim seq = 0. X iff ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ) thus ( seq is convergent & lim seq = 0. X implies ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ) ::_thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 implies ( seq is convergent & lim seq = 0. X ) ) proof assume A1: ( seq is convergent & lim seq = 0. X ) ; ::_thesis: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) then lim ||.seq.|| = ||.(0. X).|| by LOPBAN_1:20; hence ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) by A1, LOPBAN_1:20, NORMSP_1:1; ::_thesis: verum end; assume A2: ( ||.seq.|| is convergent & lim ||.seq.|| = 0 ) ; ::_thesis: ( seq is convergent & lim seq = 0. X ) A3: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_ ex_m_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_m_<=_n_holds_ ||.((seq_._n)_-_(0._X)).||_<_p let p be Real; ::_thesis: ( 0 < p implies ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((seq . n) - (0. X)).|| < p ) assume 0 < p ; ::_thesis: ex m being Element of NAT st for n being Element of NAT st m <= n holds ||.((seq . n) - (0. X)).|| < p then consider m being Element of NAT such that A4: for n being Element of NAT st m <= n holds abs ((||.seq.|| . n) - 0) < p by A2, SEQ_2:def_7; take m = m; ::_thesis: for n being Element of NAT st m <= n holds ||.((seq . n) - (0. X)).|| < p hereby ::_thesis: verum let n be Element of NAT ; ::_thesis: ( m <= n implies ||.((seq . n) - (0. X)).|| < p ) assume m <= n ; ::_thesis: ||.((seq . n) - (0. X)).|| < p then abs ((||.seq.|| . n) - 0) < p by A4; then A5: abs ||.(seq . n).|| < p by NORMSP_0:def_4; 0 <= ||.(seq . n).|| by NORMSP_1:4; then ||.(seq . n).|| < p by A5, ABSVALUE:def_1; hence ||.((seq . n) - (0. X)).|| < p by RLVECT_1:13; ::_thesis: verum end; end; then seq is convergent by NORMSP_1:def_6; hence ( seq is convergent & lim seq = 0. X ) by A3, NORMSP_1:def_7; ::_thesis: verum end; Lm18: for x being Real for vx being Element of (REAL-NS 2) st vx = <*x,0*> holds ||.vx.|| = abs x proof let x be Real; ::_thesis: for vx being Element of (REAL-NS 2) st vx = <*x,0*> holds ||.vx.|| = abs x let vx be Element of (REAL-NS 2); ::_thesis: ( vx = <*x,0*> implies ||.vx.|| = abs x ) reconsider xx = <*x,0*> as Element of REAL 2 by FINSEQ_2:101; reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22; assume vx = <*x,0*> ; ::_thesis: ||.vx.|| = abs x then A1: ||.vx.|| = |.xx.| by REAL_NS1:1; xx1 `2 = 0 by FINSEQ_1:44; then A2: (sqr xx) . 2 = 0 ^2 by VALUED_1:11; xx1 `1 = x by FINSEQ_1:44; then ( len (sqr xx) = 2 & (sqr xx) . 1 = x ^2 ) by CARD_1:def_7, VALUED_1:11; then sqr xx = <*(x ^2),(0 ^2)*> by A2, FINSEQ_1:44; then sqrt (Sum (sqr xx)) = sqrt ((x ^2) + (0 ^2)) by RVSUM_1:77 .= sqrt ((x ^2) + (0 * 0)) by SQUARE_1:def_1 ; hence ||.vx.|| = abs x by A1, COMPLEX1:72; ::_thesis: verum end; Lm19: for x being Real for vx being Element of (REAL-NS 2) st vx = <*0,x*> holds ||.vx.|| = abs x proof let x be Real; ::_thesis: for vx being Element of (REAL-NS 2) st vx = <*0,x*> holds ||.vx.|| = abs x let vx be Element of (REAL-NS 2); ::_thesis: ( vx = <*0,x*> implies ||.vx.|| = abs x ) reconsider xx = <*0,x*> as Element of REAL 2 by FINSEQ_2:101; reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22; assume vx = <*0,x*> ; ::_thesis: ||.vx.|| = abs x then A1: ||.vx.|| = |.xx.| by REAL_NS1:1; xx1 `2 = x by FINSEQ_1:44; then A2: (sqr xx) . 2 = x ^2 by VALUED_1:11; xx1 `1 = 0 by FINSEQ_1:44; then ( len (sqr xx) = 2 & (sqr xx) . 1 = 0 ^2 ) by CARD_1:def_7, VALUED_1:11; then sqr xx = <*(0 ^2),(x ^2)*> by A2, FINSEQ_1:44; then sqrt (Sum (sqr xx)) = sqrt ((0 ^2) + (x ^2)) by RVSUM_1:77 .= sqrt ((0 * 0) + (x ^2)) by SQUARE_1:def_1 .= sqrt (x ^2) ; hence ||.vx.|| = abs x by A1, COMPLEX1:72; ::_thesis: verum end; Lm20: for x being Real for vx being Element of (REAL-NS 1) st vx = <*x*> holds ||.vx.|| = abs x proof let x be Real; ::_thesis: for vx being Element of (REAL-NS 1) st vx = <*x*> holds ||.vx.|| = abs x let vx be Element of (REAL-NS 1); ::_thesis: ( vx = <*x*> implies ||.vx.|| = abs x ) reconsider xx = vx as Element of REAL 1 by REAL_NS1:def_4; assume vx = <*x*> ; ::_thesis: ||.vx.|| = abs x then sqrt (Sum (sqr xx)) = sqrt (Sum <*(x ^2)*>) by RVSUM_1:55; then A1: sqrt (Sum (sqr xx)) = sqrt (x ^2) by RVSUM_1:73; ||.vx.|| = |.xx.| by REAL_NS1:1; hence ||.vx.|| = abs x by A1, COMPLEX1:72; ::_thesis: verum end; Lm21: for v being Element of (REAL-NS 1) holds abs ((proj (1,1)) . v) = ||.v.|| proof let v be Element of (REAL-NS 1); ::_thesis: abs ((proj (1,1)) . v) = ||.v.|| reconsider x = (proj (1,1)) . v as Real ; reconsider w = v as Element of REAL 1 by REAL_NS1:def_4; ( len w = 1 & w . 1 = x ) by CARD_1:def_7, PDIFF_1:def_1; then <*x*> = w by FINSEQ_1:40; hence abs ((proj (1,1)) . v) = ||.v.|| by Lm20; ::_thesis: verum end; theorem Th5: :: CFDIFF_2:5 for u being PartFunc of (REAL 2),REAL for x0, y0 being Real for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) proof reconsider ey0 = <*0,1*> as Point of (REAL-NS 2) by Lm9; reconsider ex0 = <*1,0*> as Point of (REAL-NS 2) by Lm9; let u be PartFunc of (REAL 2),REAL; ::_thesis: for x0, y0 being Real for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) let x0, y0 be Real; ::_thesis: for xy0 being Element of REAL 2 st xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 holds ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) let xy0 be Element of REAL 2; ::_thesis: ( xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 implies ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) ) assume that A1: xy0 = <*x0,y0*> and A2: <>* u is_differentiable_in xy0 ; ::_thesis: ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) set W = (proj (1,1)) " ; consider g being PartFunc of (REAL-NS 2),(REAL-NS 1), gxy0 being Point of (REAL-NS 2) such that A3: <>* u = g and A4: xy0 = gxy0 and A5: g is_differentiable_in gxy0 by A2, PDIFF_1:def_7; consider N being Neighbourhood of gxy0 such that A6: N c= dom g and A7: ex R being RestFunc of (REAL-NS 2),(REAL-NS 1) st for xy being Point of (REAL-NS 2) st xy in N holds (g /. xy) - (g /. gxy0) = ((diff (g,gxy0)) . (xy - gxy0)) + (R /. (xy - gxy0)) by A5, NDIFF_1:def_7; consider R being RestFunc of (REAL-NS 2),(REAL-NS 1) such that A8: for xy being Point of (REAL-NS 2) st xy in N holds (g /. xy) - (g /. gxy0) = ((diff (g,gxy0)) . (xy - gxy0)) + (R /. (xy - gxy0)) by A7; consider r0 being Real such that A9: 0 < r0 and A10: { xy where xy is Point of (REAL-NS 2) : ||.(xy - gxy0).|| < r0 } c= N by NFCONT_1:def_1; consider f being PartFunc of (REAL-NS 2),(REAL-NS 1), fxy0 being Point of (REAL-NS 2) such that A11: ( <>* u = f & xy0 = fxy0 ) and A12: diff ((<>* u),xy0) = diff (f,fxy0) by A2, PDIFF_1:def_8; rng u c= dom ((proj (1,1)) ") by PDIFF_1:2; then A13: dom (<>* u) = dom u by RELAT_1:27; A14: for xy being Element of REAL 2 for L1, R1 being Real for z being Element of REAL 2 st xy in N & z = xy - xy0 & <*L1*> = (diff ((<>* u),xy0)) . z & <*R1*> = R . z holds (u . xy) - (u . xy0) = L1 + R1 proof let xy be Element of REAL 2; ::_thesis: for L1, R1 being Real for z being Element of REAL 2 st xy in N & z = xy - xy0 & <*L1*> = (diff ((<>* u),xy0)) . z & <*R1*> = R . z holds (u . xy) - (u . xy0) = L1 + R1 let L1, R1 be Real; ::_thesis: for z being Element of REAL 2 st xy in N & z = xy - xy0 & <*L1*> = (diff ((<>* u),xy0)) . z & <*R1*> = R . z holds (u . xy) - (u . xy0) = L1 + R1 let z be Element of REAL 2; ::_thesis: ( xy in N & z = xy - xy0 & <*L1*> = (diff ((<>* u),xy0)) . z & <*R1*> = R . z implies (u . xy) - (u . xy0) = L1 + R1 ) assume that A15: xy in N and A16: z = xy - xy0 and A17: <*L1*> = (diff ((<>* u),xy0)) . z and A18: <*R1*> = R . z ; ::_thesis: (u . xy) - (u . xy0) = L1 + R1 reconsider zxy = xy as Point of (REAL-NS 2) by REAL_NS1:def_4; A19: zxy - gxy0 = z by A4, A16, REAL_NS1:5; R is total by NDIFF_1:def_5; then dom R = the carrier of (REAL-NS 2) by PARTFUN1:def_2; then R /. (zxy - gxy0) = <*R1*> by A18, A19, PARTFUN1:def_6; then A20: ((diff (g,gxy0)) . (zxy - gxy0)) + (R /. (zxy - gxy0)) = <*(L1 + R1)*> by A3, A4, A11, A12, A17, A19, Lm6; A21: xy0 in N by A4, NFCONT_1:4; then A22: g /. gxy0 = g . xy0 by A4, A6, PARTFUN1:def_6 .= (<>* u) /. xy0 by A3, A6, A21, PARTFUN1:def_6 ; A23: g /. zxy = g . xy by A6, A15, PARTFUN1:def_6 .= (<>* u) /. xy by A3, A6, A15, PARTFUN1:def_6 ; A24: (g /. zxy) - (g /. gxy0) = ((diff (g,gxy0)) . (zxy - gxy0)) + (R /. (zxy - gxy0)) by A8, A15; A25: (<>* u) /. xy0 = (<>* u) . xy0 by A3, A6, A21, PARTFUN1:def_6 .= <*(u . xy0)*> by A3, A6, A13, A21, Lm12 ; (<>* u) /. xy = (<>* u) . xy by A3, A6, A15, PARTFUN1:def_6 .= <*(u . xy)*> by A3, A6, A13, A15, Lm12 ; then (g /. zxy) - (g /. gxy0) = <*(u . xy)*> - <*(u . xy0)*> by A23, A22, A25, REAL_NS1:5 .= <*(u . xy)*> + <*(- (u . xy0))*> by RVSUM_1:20 .= <*((u . xy) - (u . xy0))*> by RVSUM_1:13 ; hence (u . xy) - (u . xy0) = <*(L1 + R1)*> . 1 by A24, A20, FINSEQ_1:def_8 .= L1 + R1 by FINSEQ_1:def_8 ; ::_thesis: verum end; set Nx0 = ].(x0 - r0),(x0 + r0).[; reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by A9, RCOMP_1:def_6; A26: 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 ) reconsider xy = <*x,y0*> as Point of (REAL-NS 2) by Lm9; reconsider xx = <*(x - x0),0*> as Element of REAL 2 by FINSEQ_2:101; reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22; assume x in Nx0 ; ::_thesis: <*x,y0*> in N then A27: |.(x - x0).| < r0 by RCOMP_1:1; xx1 `2 = 0 by FINSEQ_1:44; then A28: abs (xx1 `2) = 0 by ABSVALUE:2; xy - gxy0 = <*(x - x0),(y0 - y0)*> by A1, A4, Lm10 .= <*(x - x0),0*> ; then A29: ||.(xy - gxy0).|| = |.xx.| by REAL_NS1:1; ( abs (xx1 `1) = |.(x - x0).| & |.xx.| <= (abs (xx1 `1)) + (abs (xx1 `2)) ) by FINSEQ_1:44, JGRAPH_1:31; then ||.(xy - gxy0).|| < r0 by A27, A28, A29, XXREAL_0:2; then xy in { z where z is Point of (REAL-NS 2) : ||.(z - gxy0).|| < r0 } ; hence <*x,y0*> in N by A10; ::_thesis: verum end; now__::_thesis:_for_s_being_set_st_s_in_(reproj_(1,xy0))_.:_Nx0_holds_ s_in_dom_u let s be set ; ::_thesis: ( s in (reproj (1,xy0)) .: Nx0 implies s in dom u ) assume s in (reproj (1,xy0)) .: Nx0 ; ::_thesis: s in dom u then consider x being Element of REAL such that A30: x in Nx0 and A31: s = (reproj (1,xy0)) . x by FUNCT_2:65; A32: <*x,y0*> in N by A26, A30; s = Replace (xy0,1,x) by A31, PDIFF_1:def_5 .= <*x,y0*> by A1, FINSEQ_7:13 ; hence s in dom u by A3, A6, A13, A32; ::_thesis: verum end; then ( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom u ) by FUNCT_2:def_1, TARSKI:def_3; then A33: Nx0 c= dom (u * (reproj (1,xy0))) by FUNCT_3:3; defpred S1[ Element of REAL , Element of REAL ] means ex vx being Element of REAL 2 st ( vx = <*$1,0*> & <*$2*> = R . vx ); A34: now__::_thesis:_for_x_being_Element_of_REAL_ex_y_being_Element_of_REAL_st_S1[x,y] let x be Element of REAL ; ::_thesis: ex y being Element of REAL st S1[x,y] reconsider vx = <*x,0*> as Element of REAL 2 by FINSEQ_2:101; R is total by NDIFF_1:def_5; then A35: dom R = the carrier of (REAL-NS 2) by PARTFUN1:def_2; vx is Element of (REAL-NS 2) by REAL_NS1:def_4; then R . vx in the carrier of (REAL-NS 1) by A35, PARTFUN1:4; then R . vx is Element of REAL 1 by REAL_NS1:def_4; then consider y being Element of REAL such that A36: <*y*> = R . vx by FINSEQ_2:97; take y = y; ::_thesis: S1[x,y] thus S1[x,y] by A36; ::_thesis: verum end; consider R1 being Function of REAL,REAL such that A37: for x being Element of REAL holds S1[x,R1 . x] from FUNCT_2:sch_3(A34); A38: now__::_thesis:_for_x_being_Real for_vx_being_Element_of_REAL_2_st_vx_=_<*x,0*>_holds_ <*(R1_._x)*>_=_R_._vx let x be Real; ::_thesis: for vx being Element of REAL 2 st vx = <*x,0*> holds <*(R1 . x)*> = R . vx let vx be Element of REAL 2; ::_thesis: ( vx = <*x,0*> implies <*(R1 . x)*> = R . vx ) assume A39: vx = <*x,0*> ; ::_thesis: <*(R1 . x)*> = R . vx ex vx1 being Element of REAL 2 st ( vx1 = <*x,0*> & <*(R1 . x)*> = R . vx1 ) by A37; hence <*(R1 . x)*> = R . vx by A39; ::_thesis: verum end; for h being non-zero 0 -convergent Real_Sequence holds ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) proof let h be non-zero 0 -convergent Real_Sequence; ::_thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) defpred S2[ Element of NAT , Element of (REAL-NS 2)] means $2 = <*(h . $1),0*>; A40: now__::_thesis:_for_n_being_Element_of_NAT_ex_y_being_Element_of_(REAL-NS_2)_st_S2[n,y] let n be Element of NAT ; ::_thesis: ex y being Element of (REAL-NS 2) st S2[n,y] <*(h . n),0*> in REAL 2 by FINSEQ_2:101; then reconsider y = <*(h . n),0*> as Element of (REAL-NS 2) by REAL_NS1:def_4; take y = y; ::_thesis: S2[n,y] thus S2[n,y] ; ::_thesis: verum end; consider h1 being Function of NAT,(REAL-NS 2) such that A41: for n being Element of NAT holds S2[n,h1 . n] from FUNCT_2:sch_3(A40); reconsider h1 = h1 as sequence of (REAL-NS 2) ; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.h1.||_._n_=_(abs_h)_._n let n be Element of NAT ; ::_thesis: ||.h1.|| . n = (abs h) . n A42: h1 . n = <*(h . n),0*> by A41; thus ||.h1.|| . n = ||.(h1 . n).|| by NORMSP_0:def_4 .= abs (h . n) by A42, Lm18 .= (abs h) . n by VALUED_1:18 ; ::_thesis: verum end; then A43: ||.h1.|| = abs h by FUNCT_2:63; set g = (||.h1.|| ") (#) (R /* h1); now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((||.h1.||_")_(#)_(R_/*_h1)).||_._n_=_(abs_((h_")_(#)_(R1_/*_h)))_._n let n be Element of NAT ; ::_thesis: ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R1 /* h))) . n reconsider v = h1 . n as Element of REAL 2 by REAL_NS1:def_4; dom R1 = REAL by PARTFUN1:def_2; then A44: rng h c= dom R1 ; A45: h1 . n = <*(h . n),0*> by A41; R is total by NDIFF_1:def_5; then A46: dom R = the carrier of (REAL-NS 2) by PARTFUN1:def_2; then A47: rng h1 c= dom R ; A48: h1 . n = <*(h . n),0*> by A41; A49: R /. (h1 . n) = R . v by A46, PARTFUN1:def_6 .= <*(R1 . (h . n))*> by A38, A45 ; thus ||.((||.h1.|| ") (#) (R /* h1)).|| . n = ||.(((||.h1.|| ") (#) (R /* h1)) . n).|| by NORMSP_0:def_4 .= ||.(((||.h1.|| ") . n) * ((R /* h1) . n)).|| by NDIFF_1:def_2 .= ||.(((||.h1.|| . n) ") * ((R /* h1) . n)).|| by VALUED_1:10 .= ||.((||.(h1 . n).|| ") * ((R /* h1) . n)).|| by NORMSP_0:def_4 .= ||.(((abs (h . n)) ") * ((R /* h1) . n)).|| by A48, Lm18 .= ||.(((abs (h . n)) ") * (R /. (h1 . n))).|| by A47, FUNCT_2:109 .= ||.((abs ((h . n) ")) * (R /. (h1 . n))).|| by COMPLEX1:66 .= (abs (abs ((h . n) "))) * ||.(R /. (h1 . n)).|| by NORMSP_1:def_1 .= (abs ((h . n) ")) * (abs (R1 . (h . n))) by A49, Lm20 .= abs (((h . n) ") * (R1 . (h . n))) by COMPLEX1:65 .= abs (((h . n) ") * ((R1 /* h) . n)) by A44, FUNCT_2:108 .= abs (((h ") . n) * ((R1 /* h) . n)) by VALUED_1:10 .= abs (((h ") (#) (R1 /* h)) . n) by VALUED_1:5 .= (abs ((h ") (#) (R1 /* h))) . n by VALUED_1:18 ; ::_thesis: verum end; then A50: abs ((h ") (#) (R1 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).|| by FUNCT_2:63; now__::_thesis:_for_n_being_Element_of_NAT_holds_h1_._n_<>_0._(REAL-NS_2) let n be Element of NAT ; ::_thesis: h1 . n <> 0. (REAL-NS 2) A51: h . n <> 0 by SEQ_1:5; A52: h1 . n = <*(h . n),0*> by A41; now__::_thesis:_not_h1_._n_=_0._(REAL-NS_2) assume h1 . n = 0. (REAL-NS 2) ; ::_thesis: contradiction then h1 . n = 0* 2 by REAL_NS1:def_4 .= <*0,0*> by EUCLID:54, EUCLID:70 ; hence contradiction by A52, A51, FINSEQ_1:77; ::_thesis: verum end; hence h1 . n <> 0. (REAL-NS 2) ; ::_thesis: verum end; then A53: h1 is non-zero by NDIFF_1:7; ( h is convergent & lim h = 0 ) ; then ( abs h is convergent & lim (abs h) = 0 ) by Th3; then ( h1 is convergent & lim h1 = 0. (REAL-NS 2) ) by A43, Th4; then ( h1 is 0. (REAL-NS 2) -convergent & h1 is non-zero ) by A53, NDIFF_1:def_4; then ( (||.h1.|| ") (#) (R /* h1) is convergent & lim ((||.h1.|| ") (#) (R /* h1)) = 0. (REAL-NS 1) ) by NDIFF_1:def_5; then ( ||.((||.h1.|| ") (#) (R /* h1)).|| is convergent & lim ||.((||.h1.|| ") (#) (R /* h1)).|| = 0 ) by Th4; hence ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by A50, Th3; ::_thesis: verum end; then reconsider R1 = R1 as RestFunc by FDIFF_1:def_2; ex0 is Element of REAL 2 by REAL_NS1:def_4; then (diff ((<>* u),xy0)) . ex0 is Element of REAL 1 by FUNCT_2:5; then consider Dux being Real such that A54: <*Dux*> = (diff ((<>* u),xy0)) . ex0 by FINSEQ_2:97; deffunc H1( Real) -> Element of REAL = Dux * $1; consider LD1 being Function of REAL,REAL such that A55: for x being Real holds LD1 . x = H1(x) from FUNCT_2:sch_4(); set Ny0 = ].(y0 - r0),(y0 + r0).[; reconsider Ny0 = ].(y0 - r0),(y0 + r0).[ as Neighbourhood of y0 by A9, RCOMP_1:def_6; A56: 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 ) reconsider xy = <*x0,y*> as Point of (REAL-NS 2) by Lm9; reconsider xx = <*0,(y - y0)*> as Element of REAL 2 by FINSEQ_2:101; reconsider xx1 = xx as Point of (TOP-REAL 2) by EUCLID:22; assume y in Ny0 ; ::_thesis: <*x0,y*> in N then A57: |.(y - y0).| < r0 by RCOMP_1:1; xx1 `1 = 0 by FINSEQ_1:44; then A58: abs (xx1 `1) = 0 by ABSVALUE:2; |.xx.| <= (abs (xx1 `1)) + (abs (xx1 `2)) by JGRAPH_1:31; then A59: |.xx.| <= |.(y - y0).| by A58, FINSEQ_1:44; xy - gxy0 = <*(x0 - x0),(y - y0)*> by A1, A4, Lm10 .= <*0,(y - y0)*> ; then ||.(xy - gxy0).|| = |.xx.| by REAL_NS1:1; then ||.(xy - gxy0).|| < r0 by A57, A59, XXREAL_0:2; then xy in { z where z is Point of (REAL-NS 2) : ||.(z - gxy0).|| < r0 } ; hence <*x0,y*> in N by A10; ::_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 A60: y in Ny0 and A61: s = (reproj (2,xy0)) . y by FUNCT_2:65; A62: <*x0,y*> in N by A56, A60; s = Replace (xy0,2,y) by A61, PDIFF_1:def_5 .= <*x0,y*> by A1, FINSEQ_7:14 ; hence s in dom u by A3, A6, A13, A62; ::_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 A63: Ny0 c= dom (u * (reproj (2,xy0))) by FUNCT_3:3; defpred S2[ Element of REAL , Element of REAL ] means ex vy being Element of REAL 2 st ( vy = <*0,$1*> & <*$2*> = R . vy ); A64: now__::_thesis:_for_x_being_Element_of_REAL_ex_y_being_Element_of_REAL_st_S2[x,y] let x be Element of REAL ; ::_thesis: ex y being Element of REAL st S2[x,y] reconsider vx = <*0,x*> as Element of REAL 2 by FINSEQ_2:101; R is total by NDIFF_1:def_5; then A65: dom R = the carrier of (REAL-NS 2) by PARTFUN1:def_2; vx is Element of (REAL-NS 2) by REAL_NS1:def_4; then R . vx in the carrier of (REAL-NS 1) by A65, PARTFUN1:4; then R . vx is Element of REAL 1 by REAL_NS1:def_4; then consider y being Element of REAL such that A66: <*y*> = R . vx by FINSEQ_2:97; take y = y; ::_thesis: S2[x,y] thus S2[x,y] by A66; ::_thesis: verum end; consider R3 being Function of REAL,REAL such that A67: for x being Element of REAL holds S2[x,R3 . x] from FUNCT_2:sch_3(A64); A68: now__::_thesis:_for_y_being_Real for_vy_being_Element_of_REAL_2_st_vy_=_<*0,y*>_holds_ <*(R3_._y)*>_=_R_._vy let y be Real; ::_thesis: for vy being Element of REAL 2 st vy = <*0,y*> holds <*(R3 . y)*> = R . vy let vy be Element of REAL 2; ::_thesis: ( vy = <*0,y*> implies <*(R3 . y)*> = R . vy ) assume A69: vy = <*0,y*> ; ::_thesis: <*(R3 . y)*> = R . vy ex vy1 being Element of REAL 2 st ( vy1 = <*0,y*> & <*(R3 . y)*> = R . vy1 ) by A67; hence <*(R3 . y)*> = R . vy by A69; ::_thesis: verum end; 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 ) defpred S3[ Element of NAT , Element of (REAL-NS 2)] means $2 = <*0,(h . $1)*>; A70: now__::_thesis:_for_n_being_Element_of_NAT_ex_y_being_Element_of_(REAL-NS_2)_st_S3[n,y] let n be Element of NAT ; ::_thesis: ex y being Element of (REAL-NS 2) st S3[n,y] <*0,(h . n)*> in REAL 2 by FINSEQ_2:101; then reconsider y = <*0,(h . n)*> as Element of (REAL-NS 2) by REAL_NS1:def_4; take y = y; ::_thesis: S3[n,y] thus S3[n,y] ; ::_thesis: verum end; consider h1 being Function of NAT,(REAL-NS 2) such that A71: for n being Element of NAT holds S3[n,h1 . n] from FUNCT_2:sch_3(A70); reconsider h1 = h1 as sequence of (REAL-NS 2) ; now__::_thesis:_for_n_being_Element_of_NAT_holds_||.h1.||_._n_=_(abs_h)_._n let n be Element of NAT ; ::_thesis: ||.h1.|| . n = (abs h) . n A72: h1 . n = <*0,(h . n)*> by A71; thus ||.h1.|| . n = ||.(h1 . n).|| by NORMSP_0:def_4 .= abs (h . n) by A72, Lm19 .= (abs h) . n by VALUED_1:18 ; ::_thesis: verum end; then A73: ||.h1.|| = abs h by FUNCT_2:63; set g = (||.h1.|| ") (#) (R /* h1); now__::_thesis:_for_n_being_Element_of_NAT_holds_||.((||.h1.||_")_(#)_(R_/*_h1)).||_._n_=_(abs_((h_")_(#)_(R3_/*_h)))_._n let n be Element of NAT ; ::_thesis: ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R3 /* h))) . n reconsider v = h1 . n as Element of REAL 2 by REAL_NS1:def_4; dom R3 = REAL by PARTFUN1:def_2; then A74: rng h c= dom R3 ; A75: h1 . n = <*0,(h . n)*> by A71; R is total by NDIFF_1:def_5; then A76: dom R = the carrier of (REAL-NS 2) by PARTFUN1:def_2; then A77: rng h1 c= dom R ; A78: h1 . n = <*0,(h . n)*> by A71; A79: R /. (h1 . n) = R . v by A76, PARTFUN1:def_6 .= <*(R3 . (h . n))*> by A68, A75 ; thus ||.((||.h1.|| ") (#) (R /* h1)).|| . n = ||.(((||.h1.|| ") (#) (R /* h1)) . n).|| by NORMSP_0:def_4 .= ||.(((||.h1.|| ") . n) * ((R /* h1) . n)).|| by NDIFF_1:def_2 .= ||.(((||.h1.|| . n) ") * ((R /* h1) . n)).|| by VALUED_1:10 .= ||.((||.(h1 . n).|| ") * ((R /* h1) . n)).|| by NORMSP_0:def_4 .= ||.(((abs (h . n)) ") * ((R /* h1) . n)).|| by A78, Lm19 .= ||.(((abs (h . n)) ") * (R /. (h1 . n))).|| by A77, FUNCT_2:109 .= ||.((abs ((h . n) ")) * (R /. (h1 . n))).|| by COMPLEX1:66 .= (abs (abs ((h . n) "))) * ||.(R /. (h1 . n)).|| by NORMSP_1:def_1 .= (abs ((h . n) ")) * (abs (R3 . (h . n))) by A79, Lm20 .= abs (((h . n) ") * (R3 . (h . n))) by COMPLEX1:65 .= abs (((h . n) ") * ((R3 /* h) . n)) by A74, FUNCT_2:108 .= abs (((h ") . n) * ((R3 /* h) . n)) by VALUED_1:10 .= abs (((h ") (#) (R3 /* h)) . n) by VALUED_1:5 .= (abs ((h ") (#) (R3 /* h))) . n by VALUED_1:18 ; ::_thesis: verum end; then A80: abs ((h ") (#) (R3 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).|| by FUNCT_2:63; now__::_thesis:_for_n_being_Element_of_NAT_holds_h1_._n_<>_0._(REAL-NS_2) let n be Element of NAT ; ::_thesis: h1 . n <> 0. (REAL-NS 2) A81: h . n <> 0 by SEQ_1:5; A82: h1 . n = <*0,(h . n)*> by A71; now__::_thesis:_not_h1_._n_=_0._(REAL-NS_2) assume h1 . n = 0. (REAL-NS 2) ; ::_thesis: contradiction then h1 . n = 0* 2 by REAL_NS1:def_4 .= <*0,0*> by EUCLID:54, EUCLID:70 ; hence contradiction by A82, A81, FINSEQ_1:77; ::_thesis: verum end; hence h1 . n <> 0. (REAL-NS 2) ; ::_thesis: verum end; then A83: h1 is non-zero by NDIFF_1:7; ( h is convergent & lim h = 0 ) ; then ( abs h is convergent & lim (abs h) = 0 ) by Th3; then ( h1 is convergent & lim h1 = 0. (REAL-NS 2) ) by A73, Th4; then ( h1 is 0. (REAL-NS 2) -convergent & h1 is non-zero ) by A83, NDIFF_1:def_4; then ( (||.h1.|| ") (#) (R /* h1) is convergent & lim ((||.h1.|| ") (#) (R /* h1)) = 0. (REAL-NS 1) ) by NDIFF_1:def_5; then ( ||.((||.h1.|| ") (#) (R /* h1)).|| is convergent & lim ||.((||.h1.|| ") (#) (R /* h1)).|| = 0 ) by Th4; hence ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 ) by A80, Th3; ::_thesis: verum end; then reconsider R3 = R3 as RestFunc by FDIFF_1:def_2; ey0 is Element of REAL 2 by REAL_NS1:def_4; then (diff ((<>* u),xy0)) . ey0 is Element of REAL 1 by FUNCT_2:5; then consider Duy being Real such that A84: <*Duy*> = (diff ((<>* u),xy0)) . ey0 by FINSEQ_2:97; deffunc H2( Real) -> Element of REAL = Duy * $1; consider LD3 being Function of REAL,REAL such that A85: for x being Real holds LD3 . x = H2(x) from FUNCT_2:sch_4(); reconsider LD3 = LD3 as LinearFunc by A85, FDIFF_1:def_3; A86: LD3 . 1 = Duy * 1 by A85 .= Duy ; A87: 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 A1, FINSEQ_7:14 ; ::_thesis: verum end; A88: for y being Real st y in Ny0 holds ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0)) proof ey0 is Element of REAL 2 by REAL_NS1:def_4; then reconsider D1 = (diff ((<>* u),xy0)) . ey0 as Element of REAL 1 by FUNCT_2:5; let y be Real; ::_thesis: ( y in Ny0 implies ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0)) ) assume A89: y in Ny0 ; ::_thesis: ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0)) reconsider xy = <*x0,y*> as Element of REAL 2 by FINSEQ_2:101; A90: LD3 . (y - y0) = Duy * (y - y0) by A85; A91: xy - xy0 = <*(x0 - x0),(y - y0)*> by A1, Lm7 .= <*((y - y0) * 0),((y - y0) * 1)*> .= (y - y0) * ey0 by Lm11 ; A92: diff (f,fxy0) is LinearOperator of (REAL-NS 2),(REAL-NS 1) by LOPBAN_1:def_9; (y - y0) * D1 = (y - y0) * ((diff (f,fxy0)) . ey0) by A12, REAL_NS1:3 .= (diff ((<>* u),xy0)) . (xy - xy0) by A12, A91, A92, LOPBAN_1:def_5 ; then A93: <*(LD3 . (y - y0))*> = (diff ((<>* u),xy0)) . (xy - xy0) by A84, A90, RVSUM_1:47; <*0,(y - y0)*> = <*(x0 - x0),(y - y0)*> .= xy - xy0 by A1, Lm7 ; then A94: <*(R3 . (y - y0))*> = R . (xy - xy0) by A68; thus ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (u . <*x0,y*>) - ((u * (reproj (2,xy0))) . y0) by A87 .= (u . xy) - (u . xy0) by A1, A87 .= (LD3 . (y - y0)) + (R3 . (y - y0)) by A14, A56, A89, A93, A94 ; ::_thesis: verum end; reconsider LD1 = LD1 as LinearFunc by A55, FDIFF_1:def_3; A95: LD1 . 1 = Dux * 1 by A55 .= Dux ; A96: for x being Real holds (u * (reproj (1,xy0))) . x = u . <*x,y0*> proof let x be Real; ::_thesis: (u * (reproj (1,xy0))) . x = u . <*x,y0*> x in REAL ; then x in dom (reproj (1,xy0)) by PDIFF_1:def_5; hence (u * (reproj (1,xy0))) . x = u . ((reproj (1,xy0)) . x) by FUNCT_1:13 .= u . (Replace (xy0,1,x)) by PDIFF_1:def_5 .= u . <*x,y0*> by A1, FINSEQ_7:13 ; ::_thesis: verum end; A97: for x being Real st x in Nx0 holds ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) proof ex0 is Element of REAL 2 by REAL_NS1:def_4; then reconsider D1 = (diff ((<>* u),xy0)) . ex0 as Element of REAL 1 by FUNCT_2:5; let x be Real; ::_thesis: ( x in Nx0 implies ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) ) assume A98: x in Nx0 ; ::_thesis: ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) reconsider xy = <*x,y0*> as Element of REAL 2 by FINSEQ_2:101; A99: LD1 . (x - x0) = Dux * (x - x0) by A55; A100: xy - xy0 = <*(x - x0),(y0 - y0)*> by A1, Lm7 .= <*((x - x0) * 1),((x - x0) * 0)*> .= (x - x0) * ex0 by Lm11 ; A101: diff (f,fxy0) is LinearOperator of (REAL-NS 2),(REAL-NS 1) by LOPBAN_1:def_9; (x - x0) * D1 = (x - x0) * ((diff (f,fxy0)) . ex0) by A12, REAL_NS1:3 .= (diff ((<>* u),xy0)) . (xy - xy0) by A12, A100, A101, LOPBAN_1:def_5 ; then A102: <*(LD1 . (x - x0))*> = (diff ((<>* u),xy0)) . (xy - xy0) by A54, A99, RVSUM_1:47; <*(x - x0),0*> = <*(x - x0),(y0 - y0)*> .= xy - xy0 by A1, Lm7 ; then A103: <*(R1 . (x - x0))*> = R . (xy - xy0) by A38; thus ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (u . <*x,y0*>) - ((u * (reproj (1,xy0))) . x0) by A96 .= (u . xy) - (u . xy0) by A1, A96 .= (LD1 . (x - x0)) + (R1 . (x - x0)) by A14, A26, A98, A102, A103 ; ::_thesis: verum end; A104: (proj (2,2)) . xy0 = xy0 . 2 by PDIFF_1:def_1 .= y0 by A1, FINSEQ_1:44 ; then A105: u * (reproj (2,xy0)) is_differentiable_in (proj (2,2)) . xy0 by A88, A63, FDIFF_1:def_4; A106: (proj (1,2)) . xy0 = xy0 . 1 by PDIFF_1:def_1 .= x0 by A1, FINSEQ_1:44 ; then u * (reproj (1,xy0)) is_differentiable_in (proj (1,2)) . xy0 by A97, A33, FDIFF_1:def_4; hence ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) by A106, A104, A54, A84, A97, A88, A95, A33, A86, A63, A105, FDIFF_1:def_5, PDIFF_1:def_11; ::_thesis: verum end; theorem :: CFDIFF_2:6 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 v holds x + (y * ) in dom f ) & ( 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*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) holds ( f is_differentiable_in z0 & 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 v holds x + (y * ) in dom f ) & ( 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*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) holds ( f is_differentiable_in z0 & 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 v holds x + (y * ) in dom f ) & ( 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*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) holds ( f is_differentiable_in z0 & 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 v holds x + (y * ) in dom f ) & ( 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*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) holds ( f is_differentiable_in z0 & 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 v holds x + (y * ) in dom f ) & ( 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*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) holds ( f is_differentiable_in z0 & 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 v holds x + (y * ) in dom f ) & ( 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*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff (u,xy0,1) = partdiff (v,xy0,2) & partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) implies ( f is_differentiable_in z0 & 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 v holds x + (y * ) in dom f and A2: 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 A3: 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 A4: z0 = x0 + (y0 * ) and A5: xy0 = <*x0,y0*> and A6: <>* u is_differentiable_in xy0 and A7: <>* v is_differentiable_in xy0 and A8: partdiff (u,xy0,1) = partdiff (v,xy0,2) and A9: partdiff (u,xy0,2) = - (partdiff (v,xy0,1)) ; ::_thesis: ( f is_differentiable_in z0 & 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) ) A10: ex hu being PartFunc of (REAL-NS 2),(REAL-NS 1) ex huxy0 being Point of (REAL-NS 2) st ( <>* u = hu & xy0 = huxy0 & diff ((<>* u),xy0) = diff (hu,huxy0) ) by A6, PDIFF_1:def_8; A11: ex hv being PartFunc of (REAL-NS 2),(REAL-NS 1) ex hvxy0 being Point of (REAL-NS 2) st ( <>* v = hv & xy0 = hvxy0 & diff ((<>* v),xy0) = diff (hv,hvxy0) ) by A7, PDIFF_1:def_8; consider gu being PartFunc of (REAL-NS 2),(REAL-NS 1), guxy0 being Point of (REAL-NS 2) such that A12: <>* u = gu and A13: xy0 = guxy0 and A14: gu is_differentiable_in guxy0 by A6, PDIFF_1:def_7; consider Nu being Neighbourhood of guxy0 such that A15: Nu c= dom gu and A16: ex Ru being RestFunc of (REAL-NS 2),(REAL-NS 1) st for xy being Point of (REAL-NS 2) st xy in Nu holds (gu /. xy) - (gu /. guxy0) = ((diff (gu,guxy0)) . (xy - guxy0)) + (Ru /. (xy - guxy0)) by A14, NDIFF_1:def_7; consider r1 being Real such that A17: 0 < r1 and A18: { xy where xy is Point of (REAL-NS 2) : ||.(xy - guxy0).|| < r1 } c= Nu by NFCONT_1:def_1; consider gv being PartFunc of (REAL-NS 2),(REAL-NS 1), gvxy0 being Point of (REAL-NS 2) such that A19: <>* v = gv and A20: xy0 = gvxy0 and A21: gv is_differentiable_in gvxy0 by A7, PDIFF_1:def_7; consider Ru being RestFunc of (REAL-NS 2),(REAL-NS 1) such that A22: for xy being Point of (REAL-NS 2) st xy in Nu holds (gu /. xy) - (gu /. guxy0) = ((diff (gu,guxy0)) . (xy - guxy0)) + (Ru /. (xy - guxy0)) by A16; A23: ( <*(partdiff (u,xy0,1))*> = (diff ((<>* u),xy0)) . <*1,0*> & <*(partdiff (u,xy0,2))*> = (diff ((<>* u),xy0)) . <*0,1*> ) by A5, A6, Th5; A24: for x, y being Element of REAL st <*x,y*> in Nu holds (u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff (u,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) proof Ru is total by NDIFF_1:def_5; then A25: dom Ru = the carrier of (REAL-NS 2) by PARTFUN1:def_2; rng u c= dom ((proj (1,1)) ") by PDIFF_1:2; then A26: dom (<>* u) = dom u by RELAT_1:27; ||.(guxy0 - guxy0).|| < r1 by A17, NORMSP_1:6; then guxy0 in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - guxy0).|| < r1 } ; then A27: <*x0,y0*> in Nu by A5, A13, A18; then gu /. guxy0 = gu . guxy0 by A5, A13, A15, PARTFUN1:def_6 .= (<>* u) /. <*x0,y0*> by A5, A12, A13, A15, A27, PARTFUN1:def_6 .= <*(u /. <*x0,y0*>)*> by A12, A15, A26, A27, Lm13 .= <*(u . <*x0,y0*>)*> by A12, A15, A26, A27, PARTFUN1:def_6 ; then A28: (proj (1,1)) . (gu /. guxy0) = u . <*x0,y0*> by PDIFF_1:1; <*0,1*> in REAL 2 by FINSEQ_2:101; then reconsider e2 = <*0,1*> as Point of (REAL-NS 2) by REAL_NS1:def_4; <*1,0*> in REAL 2 by FINSEQ_2:101; then reconsider e1 = <*1,0*> as Point of (REAL-NS 2) by REAL_NS1:def_4; let x, y be Element of REAL ; ::_thesis: ( <*x,y*> in Nu implies (u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff (u,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) ) A29: diff (gu,guxy0) is LinearOperator of (REAL-NS 2),(REAL-NS 1) by LOPBAN_1:def_9; <*x,y*> in REAL 2 by FINSEQ_2:101; then reconsider xy = <*x,y*> as Point of (REAL-NS 2) by REAL_NS1:def_4; A30: (y - y0) * e2 = <*((y - y0) * 0),((y - y0) * 1)*> by Lm11 .= <*0,(y - y0)*> ; A31: xy - guxy0 = <*(x - x0),(y - y0)*> by A5, A13, Lm10; assume A32: <*x,y*> in Nu ; ::_thesis: (u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff (u,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) then gu /. xy = gu . xy by A15, PARTFUN1:def_6 .= (<>* u) /. <*x,y*> by A12, A15, A32, PARTFUN1:def_6 .= <*(u /. <*x,y*>)*> by A12, A15, A32, A26, Lm13 .= <*(u . <*x,y*>)*> by A12, A15, A32, A26, PARTFUN1:def_6 ; then (proj (1,1)) . (gu /. xy) = u . <*x,y*> by PDIFF_1:1; then A33: (u . <*x,y*>) - (u . <*x0,y0*>) = (proj (1,1)) . ((gu /. xy) - (gu /. guxy0)) by A28, PDIFF_1:4 .= (proj (1,1)) . (((diff (gu,guxy0)) . (xy - guxy0)) + (Ru /. (xy - guxy0))) by A22, A32 .= ((proj (1,1)) . ((diff (gu,guxy0)) . (xy - guxy0))) + ((proj (1,1)) . (Ru /. (xy - guxy0))) by PDIFF_1:4 ; (x - x0) * e1 = <*((x - x0) * 1),((x - x0) * 0)*> by Lm11 .= <*(x - x0),0*> ; then ((x - x0) * e1) + ((y - y0) * e2) = <*((x - x0) + 0),(0 + (y - y0))*> by A30, Lm10 .= <*(x - x0),(y - y0)*> ; then xy - guxy0 = ((x - x0) * e1) + ((y - y0) * e2) by A5, A13, Lm10; then (diff (gu,guxy0)) . (xy - guxy0) = ((diff (gu,guxy0)) . ((x - x0) * e1)) + ((diff (gu,guxy0)) . ((y - y0) * e2)) by A29, VECTSP_1:def_20 .= ((x - x0) * ((diff (gu,guxy0)) . e1)) + ((diff (gu,guxy0)) . ((y - y0) * e2)) by A29, LOPBAN_1:def_5 .= ((x - x0) * ((diff (gu,guxy0)) . e1)) + ((y - y0) * ((diff (gu,guxy0)) . e2)) by A29, LOPBAN_1:def_5 ; hence (u . <*x,y*>) - (u . <*x0,y0*>) = (((proj (1,1)) . ((x - x0) * ((diff (gu,guxy0)) . e1))) + ((proj (1,1)) . ((y - y0) * ((diff (gu,guxy0)) . e2)))) + ((proj (1,1)) . (Ru /. (xy - guxy0))) by A33, PDIFF_1:4 .= (((x - x0) * ((proj (1,1)) . ((diff (gu,guxy0)) . e1))) + ((proj (1,1)) . ((y - y0) * ((diff (gu,guxy0)) . e2)))) + ((proj (1,1)) . (Ru /. (xy - guxy0))) by PDIFF_1:4 .= (((x - x0) * ((proj (1,1)) . <*(partdiff (u,xy0,1))*>)) + ((y - y0) * ((proj (1,1)) . <*(partdiff (u,xy0,2))*>))) + ((proj (1,1)) . (Ru /. (xy - guxy0))) by A23, A12, A13, A10, PDIFF_1:4 .= (((x - x0) * (partdiff (u,xy0,1))) + ((y - y0) * ((proj (1,1)) . <*(partdiff (u,xy0,2))*>))) + ((proj (1,1)) . (Ru /. (xy - guxy0))) by PDIFF_1:1 .= (((x - x0) * (partdiff (u,xy0,1))) + ((y - y0) * (partdiff (u,xy0,2)))) + ((proj (1,1)) . (Ru /. (xy - guxy0))) by PDIFF_1:1 .= (((partdiff (u,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) by A31, A25, PARTFUN1:def_6 ; ::_thesis: verum end; consider Nv being Neighbourhood of gvxy0 such that A34: Nv c= dom gv and A35: ex Rv being RestFunc of (REAL-NS 2),(REAL-NS 1) st for xy being Point of (REAL-NS 2) st xy in Nv holds (gv /. xy) - (gv /. gvxy0) = ((diff (gv,gvxy0)) . (xy - gvxy0)) + (Rv /. (xy - gvxy0)) by A21, NDIFF_1:def_7; consider r2 being Real such that A36: 0 < r2 and A37: { xy where xy is Point of (REAL-NS 2) : ||.(xy - gvxy0).|| < r2 } c= Nv by NFCONT_1:def_1; set r0 = min ((r1 / 2),(r2 / 2)); set N = { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; consider Rv being RestFunc of (REAL-NS 2),(REAL-NS 1) such that A38: for xy being Point of (REAL-NS 2) st xy in Nv holds (gv /. xy) - (gv /. gvxy0) = ((diff (gv,gvxy0)) . (xy - gvxy0)) + (Rv /. (xy - gvxy0)) by A35; A39: ( <*(partdiff (v,xy0,1))*> = (diff ((<>* v),xy0)) . <*1,0*> & <*(partdiff (v,xy0,2))*> = (diff ((<>* v),xy0)) . <*0,1*> ) by A5, A7, Th5; A40: for x, y being Element of REAL st <*x,y*> in Nv holds (v . <*x,y*>) - (v . <*x0,y0*>) = (((partdiff (v,xy0,1)) * (x - x0)) + ((partdiff (v,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) proof Rv is total by NDIFF_1:def_5; then A41: dom Rv = the carrier of (REAL-NS 2) by PARTFUN1:def_2; rng v c= dom ((proj (1,1)) ") by PDIFF_1:2; then A42: dom (<>* v) = dom v by RELAT_1:27; ||.(gvxy0 - gvxy0).|| < r2 by A36, NORMSP_1:6; then gvxy0 in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 } ; then A43: <*x0,y0*> in Nv by A5, A20, A37; then gv /. gvxy0 = gv . gvxy0 by A5, A20, A34, PARTFUN1:def_6 .= (<>* v) /. <*x0,y0*> by A5, A19, A20, A34, A43, PARTFUN1:def_6 .= <*(v /. <*x0,y0*>)*> by A19, A34, A42, A43, Lm13 .= <*(v . <*x0,y0*>)*> by A19, A34, A42, A43, PARTFUN1:def_6 ; then A44: (proj (1,1)) . (gv /. gvxy0) = v . <*x0,y0*> by PDIFF_1:1; <*0,1*> in REAL 2 by FINSEQ_2:101; then reconsider e2 = <*0,1*> as Point of (REAL-NS 2) by REAL_NS1:def_4; <*1,0*> in REAL 2 by FINSEQ_2:101; then reconsider e1 = <*1,0*> as Point of (REAL-NS 2) by REAL_NS1:def_4; let x, y be Element of REAL ; ::_thesis: ( <*x,y*> in Nv implies (v . <*x,y*>) - (v . <*x0,y0*>) = (((partdiff (v,xy0,1)) * (x - x0)) + ((partdiff (v,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) ) A45: diff (gv,gvxy0) is LinearOperator of (REAL-NS 2),(REAL-NS 1) by LOPBAN_1:def_9; <*x,y*> in REAL 2 by FINSEQ_2:101; then reconsider xy = <*x,y*> as Point of (REAL-NS 2) by REAL_NS1:def_4; A46: (y - y0) * e2 = <*((y - y0) * 0),((y - y0) * 1)*> by Lm11 .= <*0,(y - y0)*> ; A47: xy - gvxy0 = <*(x - x0),(y - y0)*> by A5, A20, Lm10; assume A48: <*x,y*> in Nv ; ::_thesis: (v . <*x,y*>) - (v . <*x0,y0*>) = (((partdiff (v,xy0,1)) * (x - x0)) + ((partdiff (v,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) then gv /. xy = gv . xy by A34, PARTFUN1:def_6 .= (<>* v) /. <*x,y*> by A19, A34, A48, PARTFUN1:def_6 .= <*(v /. <*x,y*>)*> by A19, A34, A48, A42, Lm13 .= <*(v . <*x,y*>)*> by A19, A34, A48, A42, PARTFUN1:def_6 ; then (proj (1,1)) . (gv /. xy) = v . <*x,y*> by PDIFF_1:1; then A49: (v . <*x,y*>) - (v . <*x0,y0*>) = (proj (1,1)) . ((gv /. xy) - (gv /. gvxy0)) by A44, PDIFF_1:4 .= (proj (1,1)) . (((diff (gv,gvxy0)) . (xy - gvxy0)) + (Rv /. (xy - gvxy0))) by A38, A48 .= ((proj (1,1)) . ((diff (gv,gvxy0)) . (xy - gvxy0))) + ((proj (1,1)) . (Rv /. (xy - gvxy0))) by PDIFF_1:4 ; (x - x0) * e1 = <*((x - x0) * 1),((x - x0) * 0)*> by Lm11 .= <*(x - x0),0*> ; then ((x - x0) * e1) + ((y - y0) * e2) = <*((x - x0) + 0),(0 + (y - y0))*> by A46, Lm10 .= <*(x - x0),(y - y0)*> ; then (diff (gv,gvxy0)) . (xy - gvxy0) = ((diff (gv,gvxy0)) . ((x - x0) * e1)) + ((diff (gv,gvxy0)) . ((y - y0) * e2)) by A47, A45, VECTSP_1:def_20 .= ((x - x0) * ((diff (gv,gvxy0)) . e1)) + ((diff (gv,gvxy0)) . ((y - y0) * e2)) by A45, LOPBAN_1:def_5 .= ((x - x0) * ((diff (gv,gvxy0)) . e1)) + ((y - y0) * ((diff (gv,gvxy0)) . e2)) by A45, LOPBAN_1:def_5 ; hence (v . <*x,y*>) - (v . <*x0,y0*>) = (((proj (1,1)) . ((x - x0) * ((diff (gv,gvxy0)) . e1))) + ((proj (1,1)) . ((y - y0) * ((diff (gv,gvxy0)) . e2)))) + ((proj (1,1)) . (Rv /. (xy - gvxy0))) by A49, PDIFF_1:4 .= (((x - x0) * ((proj (1,1)) . ((diff (gv,gvxy0)) . e1))) + ((proj (1,1)) . ((y - y0) * ((diff (gv,gvxy0)) . e2)))) + ((proj (1,1)) . (Rv /. (xy - gvxy0))) by PDIFF_1:4 .= (((x - x0) * ((proj (1,1)) . ((diff (gv,gvxy0)) . e1))) + ((y - y0) * ((proj (1,1)) . ((diff (gv,gvxy0)) . e2)))) + ((proj (1,1)) . (Rv /. (xy - gvxy0))) by PDIFF_1:4 .= (((x - x0) * (partdiff (v,xy0,1))) + ((y - y0) * ((proj (1,1)) . <*(partdiff (v,xy0,2))*>))) + ((proj (1,1)) . (Rv /. (xy - gvxy0))) by A39, A19, A20, A11, PDIFF_1:1 .= (((x - x0) * (partdiff (v,xy0,1))) + ((y - y0) * (partdiff (v,xy0,2)))) + ((proj (1,1)) . (Rv /. (xy - gvxy0))) by PDIFF_1:1 .= (((partdiff (v,xy0,1)) * (x - x0)) + ((partdiff (v,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) by A47, A41, PARTFUN1:def_6 ; ::_thesis: verum end; A50: now__::_thesis:_for_x,_y_being_Element_of_REAL_st_x_+_(y_*_)_in__{__y_where_y_is_Complex_:_|.(y_-_z0).|_<_min_((r1_/_2),(r2_/_2))__}__holds_ (f_/._(x_+_(y_*_)))_-_(f_/._(x0_+_(y0_*_)))_=_(((partdiff_(u,xy0,1))_+_(_*_(partdiff_(v,xy0,1))))_*_((x_-_x0)_+_((y_-_y0)_*_)))_+_(((proj_(1,1))_._(Ru_._<*(x_-_x0),(y_-_y0)*>))_+_(((proj_(1,1))_._(Rv_._<*(x_-_x0),(y_-_y0)*>))_*_)) let x, y be Element of REAL ; ::_thesis: ( x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } implies (f /. (x + (y * ))) - (f /. (x0 + (y0 * ))) = (((partdiff (u,xy0,1)) + ( * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * ))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * )) ) assume x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; ::_thesis: (f /. (x + (y * ))) - (f /. (x0 + (y0 * ))) = (((partdiff (u,xy0,1)) + ( * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * ))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * )) then A51: ex w being Complex st ( w = x + (y * ) & |.(w - z0).| < min ((r1 / 2),(r2 / 2)) ) ; <*x,y*> in REAL 2 by FINSEQ_2:101; then reconsider xy = <*x,y*> as Point of (REAL-NS 2) by REAL_NS1:def_4; rng v c= dom ((proj (1,1)) ") by PDIFF_1:2; then A52: dom (<>* v) = dom v by RELAT_1:27; ||.(gvxy0 - gvxy0).|| < r2 by A36, NORMSP_1:6; then gvxy0 in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 } ; then <*x0,y0*> in Nv by A5, A20, A37; then A53: x0 + (y0 * ) in dom f by A1, A19, A34, A52; then A54: x0 + (y0 * ) in dom (Re f) by COMSEQ_3:def_3; A55: x0 + (y0 * ) in dom (Im f) by A53, COMSEQ_3:def_4; A56: f . (x0 + (y0 * )) = (Re (f . (x0 + (y0 * )))) + ((Im (f . (x0 + (y0 * )))) * ) by COMPLEX1:13 .= ((Re f) . (x0 + (y0 * ))) + ((Im (f . (x0 + (y0 * )))) * ) by A54, COMSEQ_3:def_3 .= ((Re f) . (x0 + (y0 * ))) + (((Im f) . (x0 + (y0 * ))) * ) by A55, COMSEQ_3:def_4 ; abs (y - y0) <= |.((x - x0) + ((y - y0) * )).| by Lm16; then A57: abs (y - y0) < min ((r1 / 2),(r2 / 2)) by A4, A51, XXREAL_0:2; A58: min ((r1 / 2),(r2 / 2)) <= r1 / 2 by XXREAL_0:17; then A59: abs (y - y0) < r1 / 2 by A57, XXREAL_0:2; abs (x - x0) <= |.((x - x0) + ((y - y0) * )).| by Lm16; then A60: abs (x - x0) < min ((r1 / 2),(r2 / 2)) by A4, A51, XXREAL_0:2; then abs (x - x0) < r1 / 2 by A58, XXREAL_0:2; then A61: (abs (x - x0)) + (abs (y - y0)) < (r1 / 2) + (r1 / 2) by A59, XREAL_1:8; xy - guxy0 = <*(x - x0),(y - y0)*> by A5, A13, Lm10; then ||.(xy - guxy0).|| <= (abs (x - x0)) + (abs (y - y0)) by Lm17; then ||.(xy - guxy0).|| < r1 by A61, XXREAL_0:2; then xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - guxy0).|| < r1 } ; then A62: (u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff (u,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,2)) * (y - y0))) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) by A18, A24 .= (((partdiff (u,xy0,1)) * (x - x0)) + ((( * (partdiff (v,xy0,1))) * (y - y0)) * )) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) by A9 ; A63: min ((r1 / 2),(r2 / 2)) <= r2 / 2 by XXREAL_0:17; then A64: abs (y - y0) < r2 / 2 by A57, XXREAL_0:2; abs (x - x0) < r2 / 2 by A63, A60, XXREAL_0:2; then A65: (abs (x - x0)) + (abs (y - y0)) < (r2 / 2) + (r2 / 2) by A64, XREAL_1:8; xy - gvxy0 = <*(x - x0),(y - y0)*> by A5, A20, Lm10; then ||.(xy - gvxy0).|| <= (abs (x - x0)) + (abs (y - y0)) by Lm17; then ||.(xy - gvxy0).|| < r2 by A65, XXREAL_0:2; then A66: xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 } ; then A67: ((v . <*x,y*>) - (v . <*x0,y0*>)) * = ((((partdiff (v,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,1)) * (y - y0))) + ((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>))) * by A8, A37, A40; <*x,y*> in Nv by A37, A66; then A68: x + (y * ) in dom f by A1, A19, A34, A52; then A69: x + (y * ) in dom (Re f) by COMSEQ_3:def_3; A70: ( f /. (x + (y * )) = f . (x + (y * )) & f /. (x0 + (y0 * )) = f . (x0 + (y0 * )) ) by A53, A68, PARTFUN1:def_6; A71: x + (y * ) in dom (Im f) by A68, COMSEQ_3:def_4; f . (x + (y * )) = (Re (f . (x + (y * )))) + ((Im (f . (x + (y * )))) * ) by COMPLEX1:13 .= ((Re f) . (x + (y * ))) + ((Im (f . (x + (y * )))) * ) by A69, COMSEQ_3:def_3 .= ((Re f) . (x + (y * ))) + (((Im f) . (x + (y * ))) * ) by A71, COMSEQ_3:def_4 ; then (f . (x + (y * ))) - (f . (x0 + (y0 * ))) = ((u . <*x,y*>) + (((Im f) . (x + (y * ))) * )) - (((Re f) . (x0 + (y0 * ))) + (((Im f) . (x0 + (y0 * ))) * )) by A2, A68, A56 .= ((u . <*x,y*>) + ((v . <*x,y*>) * )) - (((Re f) . (x0 + (y0 * ))) + (((Im f) . (x0 + (y0 * ))) * )) by A3, A68 .= ((u . <*x,y*>) + ((v . <*x,y*>) * )) - ((u . <*x0,y0*>) + (((Im f) . (x0 + (y0 * ))) * )) by A2, A53 .= ((u . <*x,y*>) + ((v . <*x,y*>) * )) - ((u . <*x0,y0*>) + ((v . <*x0,y0*>) * )) by A3, A53 .= ((u . <*x,y*>) - (u . <*x0,y0*>)) + (((v . <*x,y*>) - (v . <*x0,y0*>)) * ) ; hence (f /. (x + (y * ))) - (f /. (x0 + (y0 * ))) = (((partdiff (u,xy0,1)) + ( * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * ))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * )) by A70, A62, A67; ::_thesis: verum end; A72: for x, y being Element of REAL st x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } holds ( abs (x - x0) < r1 / 2 & abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 ) proof let x, y be Element of REAL ; ::_thesis: ( x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } implies ( abs (x - x0) < r1 / 2 & abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 ) ) assume x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; ::_thesis: ( abs (x - x0) < r1 / 2 & abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 ) then A73: ex w being Complex st ( w = x + (y * ) & |.(w - z0).| < min ((r1 / 2),(r2 / 2)) ) ; abs (x - x0) <= |.((x - x0) + ((y - y0) * )).| by Lm16; then A74: abs (x - x0) < min ((r1 / 2),(r2 / 2)) by A4, A73, XXREAL_0:2; A75: min ((r1 / 2),(r2 / 2)) <= r1 / 2 by XXREAL_0:17; hence abs (x - x0) < r1 / 2 by A74, XXREAL_0:2; ::_thesis: ( abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 ) abs (y - y0) <= |.((x - x0) + ((y - y0) * )).| by Lm16; then A76: abs (y - y0) < min ((r1 / 2),(r2 / 2)) by A4, A73, XXREAL_0:2; hence abs (y - y0) < r1 / 2 by A75, XXREAL_0:2; ::_thesis: ( abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 ) A77: min ((r1 / 2),(r2 / 2)) <= r2 / 2 by XXREAL_0:17; hence abs (x - x0) < r2 / 2 by A74, XXREAL_0:2; ::_thesis: abs (y - y0) < r2 / 2 thus abs (y - y0) < r2 / 2 by A77, A76, XXREAL_0:2; ::_thesis: verum end; z0 in COMPLEX by XCMPLX_0:def_2; then reconsider N = { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } as Neighbourhood of z0 by A17, A36, CFDIFF_1:6, XXREAL_0:21; now__::_thesis:_for_z_being_set_st_z_in_N_holds_ z_in_dom_f let z be set ; ::_thesis: ( z in N implies z in dom f ) assume A78: z in N ; ::_thesis: z in dom f then reconsider zz = z as Complex ; set x = Re zz; set y = Im zz; (Re zz) + ((Im zz) * ) in N by A78, COMPLEX1:13; then ( abs ((Re zz) - x0) < r2 / 2 & abs ((Im zz) - y0) < r2 / 2 ) by A72; then A79: (abs ((Re zz) - x0)) + (abs ((Im zz) - y0)) < (r2 / 2) + (r2 / 2) by XREAL_1:8; <*(Re zz),(Im zz)*> in REAL 2 by FINSEQ_2:101; then reconsider xy = <*(Re zz),(Im zz)*> as Point of (REAL-NS 2) by REAL_NS1:def_4; xy - gvxy0 = <*((Re zz) - x0),((Im zz) - y0)*> by A5, A20, Lm10; then ||.(xy - gvxy0).|| <= (abs ((Re zz) - x0)) + (abs ((Im zz) - y0)) by Lm17; then ||.(xy - gvxy0).|| < r2 by A79, XXREAL_0:2; then xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 } ; then A80: <*(Re zz),(Im zz)*> in Nv by A37; rng v c= dom ((proj (1,1)) ") by PDIFF_1:2; then ( z = (Re zz) + ((Im zz) * ) & dom (<>* v) = dom v ) by COMPLEX1:13, RELAT_1:27; hence z in dom f by A1, A19, A34, A80; ::_thesis: verum end; then A81: N c= dom f by TARSKI:def_3; defpred S1[ Element of COMPLEX , Element of COMPLEX ] means $2 = ((proj (1,1)) . (Ru . <*(Re $1),(Im $1)*>)) + (((proj (1,1)) . (Rv . <*(Re $1),(Im $1)*>)) * ); reconsider a = (partdiff (u,xy0,1)) + ( * (partdiff (v,xy0,1))) as Element of COMPLEX ; deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = a * $1; consider L being Function of COMPLEX,COMPLEX such that A82: for x being Element of COMPLEX holds L . x = H1(x) from FUNCT_2:sch_4(); for z being Element of COMPLEX holds L /. z = a * z by A82; then reconsider L = L as C_LinearFunc by CFDIFF_1:def_4; A83: now__::_thesis:_for_z_being_Element_of_COMPLEX_ex_y_being_Element_of_COMPLEX_st_S1[z,y] let z be Element of COMPLEX ; ::_thesis: ex y being Element of COMPLEX st S1[z,y] reconsider y = ((proj (1,1)) . (Ru . <*(Re z),(Im z)*>)) + (((proj (1,1)) . (Rv . <*(Re z),(Im z)*>)) * ) as Element of COMPLEX ; take y = y; ::_thesis: S1[z,y] thus S1[z,y] ; ::_thesis: verum end; consider R being Function of COMPLEX,COMPLEX such that A84: for z being Element of COMPLEX holds S1[z,R . z] from FUNCT_2:sch_3(A83); for h being non-zero 0 -convergent Complex_Sequence holds ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) proof let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) A85: now__::_thesis:_for_r_being_Real_st_0_<_r_holds_ ex_M_being_Element_of_NAT_st_ for_n_being_Element_of_NAT_st_M_<=_n_holds_ |.((((h_")_(#)_(R_/*_h))_._n)_-_0c).|_<_r let r be Real; ::_thesis: ( 0 < r implies ex M being Element of NAT st for n being Element of NAT st M <= n holds |.((((h ") (#) (R /* h)) . n) - 0c).| < r ) assume A86: 0 < r ; ::_thesis: ex M being Element of NAT st for n being Element of NAT st M <= n holds |.((((h ") (#) (R /* h)) . n) - 0c).| < r Rv is total by NDIFF_1:def_5; then consider d2 being Real such that A87: d2 > 0 and A88: for z being Point of (REAL-NS 2) st z <> 0. (REAL-NS 2) & ||.z.|| < d2 holds (||.z.|| ") * ||.(Rv /. z).|| < r / 2 by A86, NDIFF_1:23; Ru is total by NDIFF_1:def_5; then consider d1 being Real such that A89: d1 > 0 and A90: for z being Point of (REAL-NS 2) st z <> 0. (REAL-NS 2) & ||.z.|| < d1 holds (||.z.|| ") * ||.(Ru /. z).|| < r / 2 by A86, NDIFF_1:23; set d = min (d1,d2); ( lim h = 0 & 0 < min (d1,d2) ) by A89, A87, CFDIFF_1:def_1, XXREAL_0:21; then consider M being Element of NAT such that A91: for n being Element of NAT st M <= n holds |.((h . n) - 0).| < min (d1,d2) by COMSEQ_2:def_6; A92: min (d1,d2) <= d2 by XXREAL_0:17; A93: min (d1,d2) <= d1 by XXREAL_0:17; now__::_thesis:_for_n_being_Element_of_NAT_st_M_<=_n_holds_ |.((((h_")_(#)_(R_/*_h))_._n)_-_0).|_<_r let n be Element of NAT ; ::_thesis: ( M <= n implies |.((((h ") (#) (R /* h)) . n) - 0).| < r ) set x = Re (h . n); set y = Im (h . n); <*(Re (h . n)),(Im (h . n))*> in REAL 2 by FINSEQ_2:101; then reconsider z = <*(Re (h . n)),(Im (h . n))*> as Point of (REAL-NS 2) by REAL_NS1:def_4; A94: z <> 0. (REAL-NS 2) proof assume z = 0. (REAL-NS 2) ; ::_thesis: contradiction then z = 0* 2 by REAL_NS1:def_4 .= <*0,0*> by EUCLID:54, EUCLID:70 ; then ( Re (h . n) = 0 & Im (h . n) = 0 ) by FINSEQ_1:77; then h . n = 0 by COMPLEX1:3, COMPLEX1:4; hence contradiction by COMSEQ_1:4; ::_thesis: verum end; h . n <> 0 by COMSEQ_1:4; then A95: 0 < |.(h . n).| by COMPLEX1:47; R /. (h . n) = ((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)) + (((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)) * ) by A84; then A96: (|.(h . n).| ") * |.(R /. (h . n)).| <= (|.(h . n).| ") * ((abs ((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>))) + (abs ((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)))) by A95, Lm15, XREAL_1:64; Ru is total by NDIFF_1:def_5; then dom Ru = the carrier of (REAL-NS 2) by PARTFUN1:def_2; then A97: abs ((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)) = abs ((proj (1,1)) . (Ru /. z)) by PARTFUN1:def_6 .= ||.(Ru /. z).|| by Lm21 ; Rv is total by NDIFF_1:def_5; then dom Rv = the carrier of (REAL-NS 2) by PARTFUN1:def_2; then A98: abs ((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)) = abs ((proj (1,1)) . (Rv /. z)) by PARTFUN1:def_6 .= ||.(Rv /. z).|| by Lm21 ; h . n = (Re (h . n)) + ((Im (h . n)) * ) by COMPLEX1:13; then A99: ||.z.|| = |.(h . n).| by Lm14; assume M <= n ; ::_thesis: |.((((h ") (#) (R /* h)) . n) - 0).| < r then A100: |.((h . n) - 0).| < min (d1,d2) by A91; then ||.z.|| < d2 by A92, A99, XXREAL_0:2; then A101: (||.z.|| ") * ||.(Rv /. z).|| < r / 2 by A88, A94; ||.z.|| < d1 by A93, A100, A99, XXREAL_0:2; then (||.z.|| ") * ||.(Ru /. z).|| < r / 2 by A90, A94; then ((|.(h . n).| ") * (abs ((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)))) + ((|.(h . n).| ") * (abs ((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)))) < (r / 2) + (r / 2) by A99, A101, A97, A98, XREAL_1:8; then (|.(h . n).| ") * |.(R /. (h . n)).| < r by A96, XXREAL_0:2; then |.((h . n) ").| * |.(R /. (h . n)).| < r by COMPLEX1:66; then A102: |.(((h . n) ") * (R /. (h . n))).| < r by COMPLEX1:65; dom R = COMPLEX by FUNCT_2:def_1; then rng h c= dom R ; then |.(((h . n) ") * ((R /* h) . n)).| < r by A102, FUNCT_2:109; then |.(((h ") . n) * ((R /* h) . n)).| < r by VALUED_1:10; hence |.((((h ") (#) (R /* h)) . n) - 0).| < r by VALUED_1:5; ::_thesis: verum end; hence ex M being Element of NAT st for n being Element of NAT st M <= n holds |.((((h ") (#) (R /* h)) . n) - 0c).| < r ; ::_thesis: verum end; then (h ") (#) (R /* h) is convergent by COMSEQ_2:def_5; hence ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by A85, COMSEQ_2:def_6; ::_thesis: verum end; then reconsider R = R as C_RestFunc by CFDIFF_1:def_3; reconsider z0 = z0 as Element of COMPLEX by XCMPLX_0:def_2; now__::_thesis:_for_z_being_Element_of_COMPLEX_st_z_in_N_holds_ (f_/._z)_-_(f_/._z0)_=_(L_/._(z_-_z0))_+_(R_/._(z_-_z0)) let z be Element of COMPLEX ; ::_thesis: ( z in N implies (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) set x = Re z; set y = Im z; A103: z = (Re z) + ((Im z) * ) by COMPLEX1:13; then A104: z - z0 = ((Re z) - x0) + (((Im z) - y0) * ) by A4; then Re (z - z0) = (Re z) - x0 by COMPLEX1:12; then A105: <*(Re (z - z0)),(Im (z - z0))*> = <*((Re z) - x0),((Im z) - y0)*> by A104, COMPLEX1:12; assume z in N ; ::_thesis: (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) hence (f /. z) - (f /. z0) = (((partdiff (u,xy0,1)) + ( * (partdiff (v,xy0,1)))) * (((Re z) - x0) + (((Im z) - y0) * ))) + (((proj (1,1)) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj (1,1)) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * )) by A4, A50, A103 .= (L /. (z - z0)) + (((proj (1,1)) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj (1,1)) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * )) by A4, A82, A103 .= (L /. (z - z0)) + (R /. (z - z0)) by A84, A105 ; ::_thesis: verum end; then f is_differentiable_in z0 by A81, CFDIFF_1:def_6; hence ( f is_differentiable_in z0 & 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) ) by A2, A3, A4, A5, Th2; ::_thesis: verum end;