let f be PartFunc of COMPLEX,COMPLEX; :: thesis:
let u, v be PartFunc of (REAL 2),REAL; :: thesis:
let z0 be Complex; :: thesis:
let x0, y0 be Real; :: thesis:
let xy0 be Element of REAL 2; :: thesis:
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:
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 REST 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 3;
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 REST 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)*>))

Ru is total by NDIFF_1:def 5;
then A25: dom Ru = the carrier of (REAL-NS 2) by PARTFUN1:def 4;
rng u c= dom ((proj (1,1)) ") by PDIFF_1:2;
then A26: dom (<>* u) = dom u by RELAT_1:46;
||.(guxy0 - guxy0).|| < r1 by A17, NORMSP_1:10;
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 8
.= (<>* u) /. <*x0,y0*> by A5, A12, A13, A15, A27, PARTFUN1:def 8
.= <*(u /. <*x0,y0*>)*> by A12, A15, A26, A27, Lm14
.= <*(u . <*x0,y0*>)*> by A12, A15, A26, A27, PARTFUN1:def 8 ;
then A28: (proj (1,1)) . (gu /. guxy0) = u . <*x0,y0*> by PDIFF_1:1;
<*0,1*> in REAL 2 by FINSEQ_2:121;
then reconsider e2 = <*0,1*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
<*1,0*> in REAL 2 by FINSEQ_2:121;
then reconsider e1 = <*1,0*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
let x, y be Element of REAL ; :: thesis:
A29: diff (gu,guxy0) is LinearOperator of (REAL-NS 2),(REAL-NS 1) by LOPBAN_1:def 10;
<*x,y*> in REAL 2 by FINSEQ_2:121;
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 Lm12
.= <*0,(y - y0)*> ;
A31: xy - guxy0 = <*(x - x0),(y - y0)*> by A5, A13, Lm11;
assume A32: <*x,y*> in Nu ; :: thesis:
then gu /. xy = gu . xy by A15, PARTFUN1:def 8
.= (<>* u) /. <*x,y*> by A12, A15, A32, PARTFUN1:def 8
.= <*(u /. <*x,y*>)*> by A12, A15, A32, A26, Lm14
.= <*(u . <*x,y*>)*> by A12, A15, A32, A26, PARTFUN1:def 8 ;
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 Lm12
.= <*(x - x0),0*> ;
then ((x - x0) * e1) + ((y - y0) * e2) = <*((x - x0) + 0),(0 + (y - y0))*> by A30, Lm11
.= <*(x - x0),(y - y0)*> ;
then xy - guxy0 = ((x - x0) * e1) + ((y - y0) * e2) by A5, A13, Lm11;
then (diff (gu,guxy0)) . (xy - guxy0) = ((diff (gu,guxy0)) . ((x - x0) * e1)) + ((diff (gu,guxy0)) . ((y - y0) * e2)) by A29, GRCAT_1:def 13
.= ((x - x0) * ((diff (gu,guxy0)) . e1)) + ((diff (gu,guxy0)) . ((y - y0) * e2)) by A29, LOPBAN_1:def 6
.= ((x - x0) * ((diff (gu,guxy0)) . e1)) + ((y - y0) * ((diff (gu,guxy0)) . e2)) by A29, LOPBAN_1:def 6 ;
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 8 ;
:: thesis:

end;

consider Nv being Neighbourhood of gvxy0 such that
A34: Nv c= dom gv and
A35: ex Rv being REST 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 3;
set r0 = min ((r1 / 2),(r2 / 2));
set N = { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ;
consider Rv being REST 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 4;
rng v c= dom ((proj (1,1)) ") by PDIFF_1:2;
then A42: dom (<>* v) = dom v by RELAT_1:46;
||.(gvxy0 - gvxy0).|| < r2 by A36, NORMSP_1:10;
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 8
.= (<>* v) /. <*x0,y0*> by A5, A19, A20, A34, A43, PARTFUN1:def 8
.= <*(v /. <*x0,y0*>)*> by A19, A34, A42, A43, Lm14
.= <*(v . <*x0,y0*>)*> by A19, A34, A42, A43, PARTFUN1:def 8 ;
then A44: (proj (1,1)) . (gv /. gvxy0) = v . <*x0,y0*> by PDIFF_1:1;
<*0,1*> in REAL 2 by FINSEQ_2:121;
then reconsider e2 = <*0,1*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
<*1,0*> in REAL 2 by FINSEQ_2:121;
then reconsider e1 = <*1,0*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
let x, y be Element of REAL ; :: thesis:
A45: diff (gv,gvxy0) is LinearOperator of (REAL-NS 2),(REAL-NS 1) by LOPBAN_1:def 10;
<*x,y*> in REAL 2 by FINSEQ_2:121;
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 Lm12
.= <*0,(y - y0)*> ;
A47: xy - gvxy0 = <*(x - x0),(y - y0)*> by A5, A20, Lm11;
assume A48: <*x,y*> in Nv ; :: thesis:
then gv /. xy = gv . xy by A34, PARTFUN1:def 8
.= (<>* v) /. <*x,y*> by A19, A34, A48, PARTFUN1:def 8
.= <*(v /. <*x,y*>)*> by A19, A34, A48, A42, Lm14
.= <*(v . <*x,y*>)*> by A19, A34, A48, A42, PARTFUN1:def 8 ;
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 Lm12
.= <*(x - x0),0*> ;
then ((x - x0) * e1) + ((y - y0) * e2) = <*((x - x0) + 0),(0 + (y - y0))*> by A46, Lm11
.= <*(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, GRCAT_1:def 13
.= ((x - x0) * ((diff (gv,gvxy0)) . e1)) + ((diff (gv,gvxy0)) . ((y - y0) * e2)) by A45, LOPBAN_1:def 6
.= ((x - x0) * ((diff (gv,gvxy0)) . e1)) + ((y - y0) * ((diff (gv,gvxy0)) . e2)) by A45, LOPBAN_1:def 6 ;
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 8 ;
:: thesis:

end;

A50: now

let x, y be Element of REAL ; :: thesis:
assume x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; :: thesis:
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:121;
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:46;
||.(gvxy0 - gvxy0).|| < r2 by A36, NORMSP_1:10;
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:29
.= ((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 Lm17;
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 Lm17;
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:10;
xy - guxy0 = <*(x - x0),(y - y0)*> by A5, A13, Lm11;
then ||.(xy - guxy0).|| <= (abs (x - x0)) + (abs (y - y0)) by Lm18;
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:10;
xy - gvxy0 = <*(x - x0),(y - y0)*> by A5, A20, Lm11;
then ||.(xy - gvxy0).|| <= (abs (x - x0)) + (abs (y - y0)) by Lm18;
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;
c1: ( f /. (x + (y * )) = f . (x + (y * )) & f /. (x0 + (y0 * )) = f . (x0 + (y0 * )) ) by A53, A68, PARTFUN1:def 8;
A70: 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:29
.= ((Re f) . (x + (y * ))) + ((Im (f . (x + (y * )))) * ) by A69, COMSEQ_3:def 3
.= ((Re f) . (x + (y * ))) + (((Im f) . (x + (y * ))) * ) by A70, 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 c1, A62, A67; :: thesis:

end;

A71: 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:
assume x + (y * ) in { y where y is Complex : |.(y - z0).| < min ((r1 / 2),(r2 / 2)) } ; :: thesis:
then A72: ex w being Complex st
( w = x + (y * ) & |.(w - z0).| < min ((r1 / 2),(r2 / 2)) ) ;
abs (x - x0) <= |.((x - x0) + ((y - y0) * )).| by Lm17;
then A73: abs (x - x0) < min ((r1 / 2),(r2 / 2)) by A4, A72, XXREAL_0:2;
A74: min ((r1 / 2),(r2 / 2)) <= r1 / 2 by XXREAL_0:17;
hence abs (x - x0) < r1 / 2 by A73, XXREAL_0:2; :: thesis:
abs (y - y0) <= |.((x - x0) + ((y - y0) * )).| by Lm17;
then A75: abs (y - y0) < min ((r1 / 2),(r2 / 2)) by A4, A72, XXREAL_0:2;
hence abs (y - y0) < r1 / 2 by A74, XXREAL_0:2; :: thesis:
A76: min ((r1 / 2),(r2 / 2)) <= r2 / 2 by XXREAL_0:17;
hence abs (x - x0) < r2 / 2 by A73, XXREAL_0:2; :: thesis:
thus abs (y - y0) < r2 / 2 by A76, A75, XXREAL_0:2; :: thesis:

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

let z be set ; :: thesis:
assume A77: z in N ; :: thesis:
then reconsider zz = z as Complex ;
set x = Re zz;
set y = Im zz;
(Re zz) + ((Im zz) * ) in N by A77, COMPLEX1:29;
then ( abs ((Re zz) - x0) < r2 / 2 & abs ((Im zz) - y0) < r2 / 2 ) by A71;
then A78: (abs ((Re zz) - x0)) + (abs ((Im zz) - y0)) < (r2 / 2) + (r2 / 2) by XREAL_1:10;
<*(Re zz),(Im zz)*> in REAL 2 by FINSEQ_2:121;
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, Lm11;
then ||.(xy - gvxy0).|| <= (abs ((Re zz) - x0)) + (abs ((Im zz) - y0)) by Lm18;
then ||.(xy - gvxy0).|| < r2 by A78, XXREAL_0:2;
then xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 } ;
then A79: <*(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:29, RELAT_1:46;
hence z in dom f by A1, A19, A34, A79; :: thesis:

end;

then A80: N c= dom f by TARSKI:def 3;
defpred S₁[ 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 Complex by XCMPLX_0:def 2;
deffunc H₁( Element of COMPLEX ) -> Element of COMPLEX = a * $1;
consider L being Function of COMPLEX,COMPLEX such that
A81: 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 by A81;
then reconsider L = L as C_LINEAR by CFDIFF_1:def 4;

A82: now

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

end;

consider R being Function of COMPLEX,COMPLEX such that
A83: for z being Element of COMPLEX holds S₁[z,R . z] from FUNCT_2:sch 10(A82);
for h being convergent_to_0 Complex_Sequence holds
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 )

proof

let h be convergent_to_0 Complex_Sequence; :: thesis:

A84: now

let r be Real; :: thesis:
assume A85: 0 < r ; :: thesis:
Rv is total by NDIFF_1:def 5;
then consider d2 being Real such that
A86: d2 > 0 and
A87: for z being Point of (REAL-NS 2) st z <> 0. (REAL-NS 2) & ||.z.|| < d2 holds
(||.z.|| ") * ||.(Rv /. z).|| < r / 2 by A85, NDIFF_1:26;
Ru is total by NDIFF_1:def 5;
then consider d1 being Real such that
A88: d1 > 0 and
A89: for z being Point of (REAL-NS 2) st z <> 0. (REAL-NS 2) & ||.z.|| < d1 holds
(||.z.|| ") * ||.(Ru /. z).|| < r / 2 by A85, NDIFF_1:26;
set d = min (d1,d2);
( lim h = 0 & 0 < min (d1,d2) ) by A88, A86, CFDIFF_1:def 1, XXREAL_0:21;
then consider M being Element of NAT such that
A90: for n being Element of NAT st M <= n holds
|.((h . n) - 0).| < min (d1,d2) by COMSEQ_2:def 5;
A91: min (d1,d2) <= d2 by XXREAL_0:17;
A92: min (d1,d2) <= d1 by XXREAL_0:17;

now

let n be Element of NAT ; :: thesis:
set x = Re (h . n);
set y = Im (h . n);
<*(Re (h . n)),(Im (h . n))*> in REAL 2 by FINSEQ_2:121;
then reconsider z = <*(Re (h . n)),(Im (h . n))*> as Point of (REAL-NS 2) by REAL_NS1:def 4;
A93: z <> 0. (REAL-NS 2)

proof

assume z = 0. (REAL-NS 2) ; :: thesis:
then z = 0* 2 by REAL_NS1:def 4
.= <*0,0*> by EUCLID:58, EUCLID:74 ;
then ( Re (h . n) = 0 & Im (h . n) = 0 ) by FINSEQ_1:98;
then h . n = 0 by COMPLEX1:9, COMPLEX1:12;
hence contradiction by COMSEQ_1:4; :: thesis:

end;

h . n <> 0 by COMSEQ_1:4;
then A94: 0 < |.(h . n).| by COMPLEX1:133;
R /. (h . n) = ((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)) + (((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)) * ) by A83;
then A95: (|.(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 A94, Lm16, XREAL_1:66;
Ru is total by NDIFF_1:def 5;
then dom Ru = the carrier of (REAL-NS 2) by PARTFUN1:def 4;
then A96: abs ((proj (1,1)) . (Ru . <*(Re (h . n)),(Im (h . n))*>)) = abs ((proj (1,1)) . (Ru /. z)) by PARTFUN1:def 8
.= ||.(Ru /. z).|| by Lm22 ;
Rv is total by NDIFF_1:def 5;
then dom Rv = the carrier of (REAL-NS 2) by PARTFUN1:def 4;
then A97: abs ((proj (1,1)) . (Rv . <*(Re (h . n)),(Im (h . n))*>)) = abs ((proj (1,1)) . (Rv /. z)) by PARTFUN1:def 8
.= ||.(Rv /. z).|| by Lm22 ;
h . n = (Re (h . n)) + ((Im (h . n)) * ) by COMPLEX1:29;
then A98: ||.z.|| = |.(h . n).| by Lm15;
assume M <= n ; :: thesis:
then A99: |.((h . n) - 0).| < min (d1,d2) by A90;
then ||.z.|| < d2 by A91, A98, XXREAL_0:2;
then A100: (||.z.|| ") * ||.(Rv /. z).|| < r / 2 by A87, A93;
||.z.|| < d1 by A92, A99, A98, XXREAL_0:2;
then (||.z.|| ") * ||.(Ru /. z).|| < r / 2 by A89, A93;
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 A98, A100, A96, A97, XREAL_1:10;
then (|.(h . n).| ") * |.(R /. (h . n)).| < r by A95, XXREAL_0:2;
then |.((h . n) ").| * |.(R /. (h . n)).| < r by COMPLEX1:152;
then A101: |.(((h . n) ") * (R /. (h . n))).| < r by COMPLEX1:151;
dom R = COMPLEX by FUNCT_2:def 1;
then rng h c= dom R ;
then |.(((h . n) ") * ((R /* h) . n)).| < r by A101, FUNCT_2:186;
then |.(((h ") . n) * ((R /* h) . n)).| < r by VALUED_1:10;
hence |.((((h ") (#) (R /* h)) . n) - 0).| < r by VALUED_1:5; :: thesis:

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:

end;

then (h ") (#) (R /* h) is convergent by COMSEQ_2:def 4;
hence ( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by A84, COMSEQ_2:def 5; :: thesis:

end;

then reconsider R = R as C_REST by CFDIFF_1:def 3;

now

let z be Complex; :: thesis:
set x = Re z;
set y = Im z;
A102: z = (Re z) + ((Im z) * ) by COMPLEX1:29;
then A103: z - z0 = ((Re z) - x0) + (((Im z) - y0) * ) by A4;
then Re (z - z0) = (Re z) - x0 by COMPLEX1:28;
then A104: <*(Re (z - z0)),(Im (z - z0))*> = <*((Re z) - x0),((Im z) - y0)*> by A103, COMPLEX1:28;
assume z in N ; :: thesis:
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, A102
.= (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, A81, A102
.= (L /. (z - z0)) + (R /. (z - z0)) by A83, A104 ;
:: thesis:

end;

then f is_differentiable_in z0 by A80, 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: