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 * <i>) in dom f ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & 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 * <i>) in dom f ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & 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 * <i>) in dom f ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & 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 * <i>) in dom f ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & 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 * <i>) in dom f ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) ) & ( for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) ) & z0 = x0 + (y0 * <i>) & 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 * <i>) in dom f and
A2: for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) and
A3: for x, y being Real st x + (y * <i>) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i>)) ) and
A4: z0 = x0 + (y0 * <i>) 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;
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;
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;
<*(In (0,REAL)),jj*> in REAL 2 by FINSEQ_2:101;
then reconsider e2 = <*0,1*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
<*jj,(In (0,REAL))*> 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;
<*(In (0,REAL)),jj*> in REAL 2 by FINSEQ_2:101;
then reconsider e2 = <*0,1*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
<*jj,(In (0,REAL))*> 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 * <i>) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } holds
(f /. (x + (y * <i>))) - (f /. (x0 + (y0 * <i>))) = (((partdiff (u,xy0,1)) + (<i> * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * <i>))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * <i>))

let x, y be Element of REAL ; :: thesis: ( x + (y * <i>) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } implies (f /. (x + (y * <i>))) - (f /. (x0 + (y0 * <i>))) = (((partdiff (u,xy0,1)) + (<i> * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * <i>))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * <i>)) )
assume x + (y * <i>) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; :: thesis: (f /. (x + (y * <i>))) - (f /. (x0 + (y0 * <i>))) = (((partdiff (u,xy0,1)) + (<i> * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * <i>))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * <i>))
then A51: ex w being Complex st
( w = x + (y * <i>) & |.(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 * <i>) in dom f by A1, A19, A34, A52;
then A54: x0 + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;
A55: x0 + (y0 * <i>) in dom (Im f) by A53, COMSEQ_3:def 4;
A56: f . (x0 + (y0 * <i>)) = (Re (f . (x0 + (y0 * <i>)))) + ((Im (f . (x0 + (y0 * <i>)))) * <i>) by COMPLEX1:13
.= ((Re f) . (x0 + (y0 * <i>))) + ((Im (f . (x0 + (y0 * <i>)))) * <i>) by A54, COMSEQ_3:def 3
.= ((Re f) . (x0 + (y0 * <i>))) + (((Im f) . (x0 + (y0 * <i>))) * <i>) by A55, COMSEQ_3:def 4 ;
|.(y - y0).| <= |.((x - x0) + ((y - y0) * <i>)).| by Lm16;
then A57: |.(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: |.(y - y0).| < r1 / 2 by A57, XXREAL_0:2;
|.(x - x0).| <= |.((x - x0) + ((y - y0) * <i>)).| by Lm16;
then A60: |.(x - x0).| < min ((r1 / 2),(r2 / 2)) by A4, A51, XXREAL_0:2;
then |.(x - x0).| < r1 / 2 by A58, XXREAL_0:2;
then A61: |.(x - x0).| + |.(y - y0).| < (r1 / 2) + (r1 / 2) by A59, XREAL_1:8;
xy - guxy0 = <*(x - x0),(y - y0)*> by A5, A13, Lm10;
then ||.(xy - guxy0).|| <= |.(x - x0).| + |.(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)) + (((<i> * (partdiff (v,xy0,1))) * (y - y0)) * <i>)) + ((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) by A9 ;
A63: min ((r1 / 2),(r2 / 2)) <= r2 / 2 by XXREAL_0:17;
then A64: |.(y - y0).| < r2 / 2 by A57, XXREAL_0:2;
|.(x - x0).| < r2 / 2 by A63, A60, XXREAL_0:2;
then A65: |.(x - x0).| + |.(y - y0).| < (r2 / 2) + (r2 / 2) by A64, XREAL_1:8;
xy - gvxy0 = <*(x - x0),(y - y0)*> by A5, A20, Lm10;
then ||.(xy - gvxy0).|| <= |.(x - x0).| + |.(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*>)) * <i> = ((((partdiff (v,xy0,1)) * (x - x0)) + ((partdiff (u,xy0,1)) * (y - y0))) + ((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>))) * <i> by A8, A37, A40;
<*x,y*> in Nv by A37, A66;
then A68: x + (y * <i>) in dom f by A1, A19, A34, A52;
then A69: x + (y * <i>) in dom (Re f) by COMSEQ_3:def 3;
A70: ( f /. (x + (y * <i>)) = f . (x + (y * <i>)) & f /. (x0 + (y0 * <i>)) = f . (x0 + (y0 * <i>)) ) by A53, A68, PARTFUN1:def 6;
A71: x + (y * <i>) in dom (Im f) by A68, COMSEQ_3:def 4;
f . (x + (y * <i>)) = (Re (f . (x + (y * <i>)))) + ((Im (f . (x + (y * <i>)))) * <i>) by COMPLEX1:13
.= ((Re f) . (x + (y * <i>))) + ((Im (f . (x + (y * <i>)))) * <i>) by A69, COMSEQ_3:def 3
.= ((Re f) . (x + (y * <i>))) + (((Im f) . (x + (y * <i>))) * <i>) by A71, COMSEQ_3:def 4 ;
then (f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((u . <*x,y*>) + (((Im f) . (x + (y * <i>))) * <i>)) - (((Re f) . (x0 + (y0 * <i>))) + (((Im f) . (x0 + (y0 * <i>))) * <i>)) by A2, A68, A56
.= ((u . <*x,y*>) + ((v . <*x,y*>) * <i>)) - (((Re f) . (x0 + (y0 * <i>))) + (((Im f) . (x0 + (y0 * <i>))) * <i>)) by A3, A68
.= ((u . <*x,y*>) + ((v . <*x,y*>) * <i>)) - ((u . <*x0,y0*>) + (((Im f) . (x0 + (y0 * <i>))) * <i>)) by A2, A53
.= ((u . <*x,y*>) + ((v . <*x,y*>) * <i>)) - ((u . <*x0,y0*>) + ((v . <*x0,y0*>) * <i>)) by A3, A53
.= ((u . <*x,y*>) - (u . <*x0,y0*>)) + (((v . <*x,y*>) - (v . <*x0,y0*>)) * <i>) ;
hence (f /. (x + (y * <i>))) - (f /. (x0 + (y0 * <i>))) = (((partdiff (u,xy0,1)) + (<i> * (partdiff (v,xy0,1)))) * ((x - x0) + ((y - y0) * <i>))) + (((proj (1,1)) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj (1,1)) . (Rv . <*(x - x0),(y - y0)*>)) * <i>)) by A70, A62, A67; :: thesis: verum

end;

A72: for x, y being Element of REAL st x + (y * <i>) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } holds
( |.(x - x0).| < r1 / 2 & |.(y - y0).| < r1 / 2 & |.(x - x0).| < r2 / 2 & |.(y - y0).| < r2 / 2 )

proof

let x, y be Element of REAL ; :: thesis: ( x + (y * <i>) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } implies ( |.(x - x0).| < r1 / 2 & |.(y - y0).| < r1 / 2 & |.(x - x0).| < r2 / 2 & |.(y - y0).| < r2 / 2 ) )
assume x + (y * <i>) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; :: thesis: ( |.(x - x0).| < r1 / 2 & |.(y - y0).| < r1 / 2 & |.(x - x0).| < r2 / 2 & |.(y - y0).| < r2 / 2 )
then A73: ex w being Complex st
( w = x + (y * <i>) & |.(w - z0).| < min ((r1 / 2),(r2 / 2)) ) ;
|.(x - x0).| <= |.((x - x0) + ((y - y0) * <i>)).| by Lm16;
then A74: |.(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 |.(x - x0).| < r1 / 2 by A74, XXREAL_0:2; :: thesis: ( |.(y - y0).| < r1 / 2 & |.(x - x0).| < r2 / 2 & |.(y - y0).| < r2 / 2 )
|.(y - y0).| <= |.((x - x0) + ((y - y0) * <i>)).| by Lm16;
then A76: |.(y - y0).| < min ((r1 / 2),(r2 / 2)) by A4, A73, XXREAL_0:2;
hence |.(y - y0).| < r1 / 2 by A75, XXREAL_0:2; :: thesis: ( |.(x - x0).| < r2 / 2 & |.(y - y0).| < r2 / 2 )
A77: min ((r1 / 2),(r2 / 2)) <= r2 / 2 by XXREAL_0:17;
hence |.(x - x0).| < r2 / 2 by A74, XXREAL_0:2; :: thesis: |.(y - y0).| < r2 / 2
thus |.(y - y0).| < r2 / 2 by A77, A76, XXREAL_0:2; :: thesis: verum

end;

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 object st z in N holds
z in dom f

let z be object ; :: 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) * <i>) in N by A78, COMPLEX1:13;
then ( |.((Re zz) - x0).| < r2 / 2 & |.((Im zz) - y0).| < r2 / 2 ) by A72;
then A79: |.((Re zz) - x0).| + |.((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).|| <= |.((Re zz) - x0).| + |.((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) * <i>) & 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 S₁[ Complex, Complex] means $2 = ((proj (1,1)) . (Ru . <*(Re $1),(Im $1)*>)) + (((proj (1,1)) . (Rv . <*(Re $1),(Im $1)*>)) * <i>);
reconsider a = (partdiff (u,xy0,1)) + (<i> * (partdiff (v,xy0,1))) as Element of COMPLEX by XCMPLX_0:def 2;
deffunc H₁( Complex) -> Element of COMPLEX = In ((a * $1),COMPLEX);
consider L being Function of COMPLEX,COMPLEX such that
A82: for x being Element of COMPLEX holds L . x = H₁(x) from FUNCT_2:sch 4();
for z being Complex holds L /. z = a * z

proof

let z be Complex; :: thesis: L /. z = a * z
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
L /. z = H₁(z) by A82;
hence L /. z = a * z ; :: thesis: verum

end;

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 S₁[z,y]

let z be Element of COMPLEX ; :: thesis: ex y being Element of COMPLEX st S₁[z,y]
reconsider y = ((proj (1,1)) . (Ru . <*(Re z),(Im z)*>)) + (((proj (1,1)) . (Rv . <*(Re z),(Im z)*>)) * <i>) as Element of COMPLEX by XCMPLX_0:def 2;
take y = y; :: thesis: S₁[z,y]
thus S₁[z,y] ; :: thesis: verum

end;

consider R being Function of COMPLEX,COMPLEX such that
A84: for z being Element of COMPLEX holds S₁[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 Nat st
for n being Nat st M <= n holds
|.((((h ") (#) (R /* h)) . n) - 0c).| < r

let r be Real; :: thesis: ( 0 < r implies ex M being Nat st
for n being Nat st M <= n holds
|.((((h ") (#) (R /* h)) . n) - 0c).| < r )
assume A86: 0 < r ; :: thesis: ex M being Nat st
for n being 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 Nat such that
A91: for n being 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 Nat st M <= n holds
|.((((h ") (#) (R /* h)) . n) - 0).| < r

let n be Nat; :: thesis: ( M <= n implies |.((((h ") (#) (R /* h)) . n) - 0).| < r )
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
set x = Re (h . nn);
set y = Im (h . nn);
<*(Re (h . nn)),(Im (h . nn))*> in REAL 2 by FINSEQ_2:101;
then reconsider z = <*(Re (h . nn)),(Im (h . nn))*> 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 . nn) = 0 & Im (h . nn) = 0 ) by FINSEQ_1:77;
then h . nn = 0 by COMPLEX1:4;
hence contradiction by COMSEQ_1:4; :: thesis: verum

end;

h . nn <> 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 . nn)),(Im (h . nn))*>)) * <i>) by A84;
then A96: (|.(h . n).| ") * |.(R /. (h . n)).| <= (|.(h . n).| ") * (|.((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)).| + |.((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: |.((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)).| = |.((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: |.((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)).| = |.((proj (1,1)) . (Rv /. z)).| by PARTFUN1:def 6
.= ||.(Rv /. z).|| by Lm21 ;
h . n = (Re (h . nn)) + ((Im (h . nn)) * <i>) 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).| ") * |.((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)).|) + ((|.(h . n).| ") * |.((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 . nn) ") * ((R /* h) . nn)).| < 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 Nat st
for n being 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;

now :: thesis: for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0))

let z be 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) * <i>) by COMPLEX1:13;
then A104: z - z0 = ((Re z) - x0) + (((Im z) - y0) * <i>) 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;
A106: z - z0 in COMPLEX by XCMPLX_0:def 2;
assume z in N ; :: thesis: (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0))
hence (f /. z) - (f /. z0) = (((partdiff (u,xy0,1)) + (<i> * (partdiff (v,xy0,1)))) * (((Re z) - x0) + (((Im z) - y0) * <i>))) + (((proj (1,1)) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj (1,1)) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * <i>)) by A4, A50, A103
.= H₁(z - z0) + (((proj (1,1)) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj (1,1)) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * <i>)) by A4, A103
.= (L /. (z - z0)) + (((proj (1,1)) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj (1,1)) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * <i>)) by A82, A106
.= (L /. (z - z0)) + (R /. (z - z0)) by A84, A105, A106 ;
:: 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