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, 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)*>))

proof

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: ( <*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 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: (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 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, LOPBAN_1:def 5
.= ((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: verum

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: ( <*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 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: (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 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, LOPBAN_1:def 5
.= ((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: verum

end;

A50: now

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: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 * <i> ) in dom f by A1, A19, A34, A52;
then A54: x0 + (y0 * <i> ) in dom (Re f) by Def1;
A55: x0 + (y0 * <i> ) in dom (Im f) by A53, Def2;
A56: f /. (x0 + (y0 * <i> )) = (Re (f /. (x0 + (y0 * <i> )))) + ((Im (f /. (x0 + (y0 * <i> )))) * <i> ) by COMPLEX1:29
.= ((Re f) . (x0 + (y0 * <i> ))) + ((Im (f /. (x0 + (y0 * <i> )))) * <i> ) by A54, Def1
.= ((Re f) . (x0 + (y0 * <i> ))) + (((Im f) . (x0 + (y0 * <i> ))) * <i> ) by A55, Def2 ;
abs (y - y0) <= |.((x - x0) + ((y - y0) * <i> )).| 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) * <i> )).| 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)) + (((<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: 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*>)) * <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 Def1;
A70: x + (y * <i> ) in dom (Im f) by A68, Def2;
f /. (x + (y * <i> )) = (Re (f /. (x + (y * <i> )))) + ((Im (f /. (x + (y * <i> )))) * <i> ) by COMPLEX1:29
.= ((Re f) . (x + (y * <i> ))) + ((Im (f /. (x + (y * <i> )))) * <i> ) by A69, Def1
.= ((Re f) . (x + (y * <i> ))) + (((Im f) . (x + (y * <i> ))) * <i> ) by A70, Def2 ;
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 A62, A67; :: thesis: verum

end;

A71: 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
( 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 * <i> ) 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 * <i> ) 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 A72: ex w being Complex st
( w = x + (y * <i> ) & |.(w - z0).| < min (r1 / 2),(r2 / 2) ) ;
abs (x - x0) <= |.((x - x0) + ((y - y0) * <i> )).| 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) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 )
abs (y - y0) <= |.((x - x0) + ((y - y0) * <i> )).| 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: ( abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 )
A76: min (r1 / 2),(r2 / 2) <= r2 / 2 by XXREAL_0:17;
hence abs (x - x0) < r2 / 2 by A73, XXREAL_0:2; :: thesis: abs (y - y0) < r2 / 2
thus abs (y - y0) < r2 / 2 by A76, A75, XXREAL_0:2; :: thesis: verum
<*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;

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: ( z in N implies z in dom f )
assume A77: 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 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) * <i> ) & dom (<>* v) = dom v ) by COMPLEX1:29, RELAT_1:46;
hence z in dom f by A1, A19, A34, A79; :: thesis: verum

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)*>)) * <i> );
reconsider a = (partdiff u,xy0,1) + (<i> * (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: 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
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: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 )

A84: now

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 A85: 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
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: ( 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: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

set m = 2;
assume z = 0. (REAL-NS 2) ; :: thesis: contradiction
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: verum

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))*>)) * <i> ) 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)) * <i> ) by COMPLEX1:29;
then A98: ||.z.|| = |.(h . n).| by Lm15;
assume M <= n ; :: thesis: |.((((h " ) (#) (R /* h)) . n) - 0 ).| < r
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: 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 4;
hence ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 ) by A84, COMSEQ_2:def 5; :: thesis: verum

end;

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

now

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;
A102: z = (Re z) + ((Im z) * <i> ) by COMPLEX1:29;
then A103: z - z0 = ((Re z) - x0) + (((Im z) - y0) * <i> ) 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: (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, A102
.= (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 A4, A81, A102
.= (L /. (z - z0)) + (R /. (z - z0)) by A83, A104 ;
:: thesis: verum

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: verum