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 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:
deffunc H₁( 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 = H₁(x) from FUNCT_2:sch 4();
reconsider LD2 = LD2 as LINEAR by A6, FDIFF_1:def 4;
deffunc H₂( 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 = H₂(x) from FUNCT_2:sch 4();
A8: for y being Real holds (v * (reproj 2,xy0)) . y = v . <*x0,y*>

let y be Real; :: thesis:
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:23
.= v . (Replace xy0,2,y) by PDIFF_1:def 5
.= v . <*x0,y*> by A4, FINSEQ_7:16 ;
:: thesis:

end;

A9: for y being Real holds (u * (reproj 2,xy0)) . y = u . <*x0,y*>

proof

let y be Real; :: thesis:
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:23
.= u . (Replace xy0,2,y) by PDIFF_1:def 5
.= u . <*x0,y*> by A4, FINSEQ_7:16 ;
:: thesis:

end;

A10: (proj 2,2) . xy0 = xy0 . 2 by PDIFF_1:def 1
.= y0 by A4, FINSEQ_1:61 ;
reconsider LD1 = LD1 as LINEAR by A7, FDIFF_1:def 4;
deffunc H₃( 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 = H₃(x) from FUNCT_2:sch 4();
for x being Real holds LD3 . x = (- (Im (diff f,z0))) * x

proof

let x be Real; :: thesis:
thus LD3 . x = - ((Im (diff f,z0)) * x) by A11
.= (- (Im (diff f,z0))) * x ; :: thesis:

end;

then reconsider LD3 = LD3 as LINEAR by FDIFF_1:def 4;
consider N being Neighbourhood of z0 such that
A12: N c= dom f and
A13: ex L being C_LINEAR ex R being C_REST st
( diff f,z0 = L /. 1r & ( for z being 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_LINEAR, R being C_REST such that
A14: ( diff f,z0 = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A13;
deffunc H₄( Real) -> Element of REAL = (Im R) . ($1 * );
consider R4 being Function of REAL ,REAL such that
A15: for y being Real holds R4 . y = H₄(y) from FUNCT_2:sch 4();
a1: 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:
assume A16: z in N ; :: thesis:
consider a0 being Complex such that
A17: for w being Complex holds L /. w = a0 * w by CFDIFF_1:def 4;
L /. (1r * (z - z0)) = (a0 * 1r ) * (z - z0) by A17
.= (L /. 1r ) * (z - z0) by A17 ;
hence (f /. z) - (f /. z0) = ((diff f,z0) * (z - z0)) + (R /. (z - z0)) by A14, A16; :: thesis:

end;

A18: 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:
assume b1: ( x + (y * ) in N & x0 + (y0 * ) in N ) ; :: thesis:
then ( x + (y * ) in dom f & x0 + (y0 * ) in dom f ) by A12;
then ( f . (x + (y * )) = f /. (x + (y * )) & f . (x0 + (y0 * )) = f /. (x0 + (y0 * )) ) by PARTFUN1:def 8;
hence (f . (x + (y * ))) - (f . (x0 + (y0 * ))) = ((diff f,z0) * ((x + (y * )) - (x0 + (y0 * )))) + (R /. ((x + (y * )) - (x0 + (y0 * )))) by a1, b1, A3; :: thesis:

end;

b2: dom R = COMPLEX by PARTFUN1:def 4;
for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R4 /* h) is convergent & lim ((h " ) (#) (R4 /* h)) = 0 )

proof

let h be convergent_to_0 Real_Sequence; :: thesis:
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz0 = h as Complex_Sequence by FUNCT_2:8;
reconsider hz0 = hz0 as convergent_to_0 Complex_Sequence by Lm4;
set hz = (#) hz0;
reconsider hz = (#) hz0 as convergent_to_0 Complex_Sequence by Lm6;

now

A19: rng hz c= dom R by b2;
dom R4 = REAL by PARTFUN1:def 4;
then A20: rng h c= dom R4 ;
let n be Element of NAT ; :: thesis:
A21: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
A22: hz . n = (h . n) * by VALUED_1:6;
(h . n) * in COMPLEX by XCMPLX_0:def 2;
then A23: (h . n) * in dom (Im R) by Th1;
thus ((h " ) (#) (R4 /* h)) . n = ((h " ) . n) * ((R4 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R4 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R4 . (h . n)) by A20, FUNCT_2:185
.= ((h . n) " ) * ((Im R) . ((h . n) * )) by A15
.= ((Re ((h . n) " )) * (Im (R . ((h . n) * )))) + ((Re (R . ((h . n) * ))) * (Im ((h . n) " ))) by A23, A21, COMSEQ_3:def 4
.= Im ((((hz . n) / ) " ) * (R . (hz . n))) by A22, COMPLEX1:24
.= Im (( / (hz . n)) * (R . (hz . n))) by XCMPLX_1:215
.= 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:24
.= Re (((hz " ) . n) * ((R /* hz) . n)) by A19, COMPLEX1:17, FUNCT_2:186
.= Re (((hz " ) (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis:

end;

then A24: (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 A24, COMPLEX1:12, COMSEQ_3:41; :: thesis:

end;

then reconsider R4 = R4 as REST by FDIFF_1:def 3;
deffunc H₅( Real) -> Element of REAL = (Re R) . ($1 * );
A25: dom R = COMPLEX by PARTFUN1:def 4;
consider R2 being Function of REAL ,REAL such that
A26: for y being Real holds R2 . y = H₅(y) from FUNCT_2:sch 4();
for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 )

proof

now

dom R = COMPLEX by PARTFUN1:def 4;
then A28: rng hz c= dom R ;
dom R2 = REAL by PARTFUN1:def 4;
then A29: rng h c= dom R2 ;
let n be Element of NAT ; :: thesis:
A30: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
A31: hz . n = (h . n) * by VALUED_1:6;
dom (Re R) = COMPLEX by Th1;
then A32: (h . n) * in dom (Re R) by XCMPLX_0:def 2;
e1: R . (hz . n) = R /. (hz . n) ;
thus ((h " ) (#) (R2 /* h)) . n = ((h " ) . n) * ((R2 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R2 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R2 . (h . n)) by A29, FUNCT_2:185
.= ((h . n) " ) * ((Re R) . ((h . n) * )) by A26
.= ((Re ((h . n) " )) * (Re (R . ((h . n) * )))) - ((Im ((h . n) " )) * (Im (R . ((h . n) * )))) by A32, A30, COMSEQ_3:def 3
.= Re ((((hz . n) / ) " ) * (R . (hz . n))) by A31, COMPLEX1:24
.= Re (( / (hz . n)) * (R . (hz . n))) by XCMPLX_1:215
.= 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:24
.= - (Im (((hz " ) . n) * ((R /* hz) . n))) by e1, A28, COMPLEX1:17, FUNCT_2:186
.= - (Im (((hz " ) (#) (R /* hz)) . n)) by VALUED_1:5
.= - ((Im ((hz " ) (#) (R /* hz))) . n) by COMSEQ_3:def 6 ; :: thesis:

end;

then A33: (h " ) (#) (R2 /* h) = - (Im ((hz " ) (#) (R /* hz))) by SEQ_1:14;
lim ((hz " ) (#) (R /* hz)) = 0 by CFDIFF_1:def 3;
then lim (Im ((hz " ) (#) (R /* hz))) = Im 0 by A27, COMSEQ_3:41;
then lim ((h " ) (#) (R2 /* h)) = - (Im 0 ) by A33, A27, SEQ_2:24
.= 0 by COMPLEX1:12 ;
hence ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 ) by A33, A27, SEQ_2:23; :: thesis:

end;

then reconsider R2 = R2 as REST by FDIFF_1:def 3;
consider r0 being Real such that
A34: 0 < r0 and
A35: { 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 A34, RCOMP_1:def 7;
A36: for y being Real st y in Ny0 holds
x0 + (y * ) in N

proof

let y be Real; :: thesis:
|.((x0 + (y * )) - z0).| = |.((y - y0) * ).| by A3;
then A37: |.((x0 + (y * )) - z0).| = |.(y - y0).| * |. .| by COMPLEX1:151;
assume y in Ny0 ; :: thesis:
then ( x0 + (y * ) is Complex & |.((x0 + (y * )) - z0).| < r0 ) by A37, COMPLEX1:135, RCOMP_1:8, XCMPLX_0:def 2;
then x0 + (y * ) in { w where w is Complex : |.(w - z0).| < r0 } ;
hence x0 + (y * ) in N by A35; :: thesis:

end;

A38: 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:
thus (diff f,z0) * ((x + (y * )) - (x0 + (y0 * ))) = ((Re (diff f,z0)) + ((Im (diff f,z0)) * )) * ((x - x0) + ((y - y0) * )) by COMPLEX1:29
.= (((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:

end;

A39: 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:
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 A38
.= ((Re (diff f,z0)) * (x - x0)) - ((Im (diff f,z0)) * (y - y0)) by COMPLEX1:28 ; :: thesis:

end;

A40: 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:
(x0 + (y * )) - (x0 + (y0 * )) in dom R by A25, XCMPLX_0:def 2;
then A41: (y - y0) * in dom (Re R) by COMSEQ_3:def 3;
assume y in Ny0 ; :: thesis:
then A43: x0 + (y * ) in N by A36;
then x0 + (y * ) in dom f by A12;
then A44: x0 + (y * ) in dom (Re f) by COMSEQ_3:def 3;
A45: x0 + (y0 * ) in N by A3, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A12;
then A46: x0 + (y0 * ) in dom (Re f) by COMSEQ_3:def 3;
(x0 + (y * )) - (x0 + (y0 * )) in COMPLEX by XCMPLX_0:def 2;
then a2: R . ((x0 + (y * )) - (x0 + (y0 * ))) = R /. ((x0 + (y * )) - (x0 + (y0 * ))) by b2, PARTFUN1:def 8;
(u . <*x0,y*>) - (u . <*x0,y0*>) = ((Re f) . (x0 + (y * ))) - (u . <*x0,y0*>) by A1, A12, A43
.= ((Re f) . (x0 + (y * ))) - ((Re f) . (x0 + (y0 * ))) by A1, A12, A45
.= (Re (f . (x0 + (y * )))) - ((Re f) . (x0 + (y0 * ))) by A44, COMSEQ_3:def 3
.= (Re (f . (x0 + (y * )))) - (Re (f . (x0 + (y0 * )))) by A46, COMSEQ_3:def 3
.= Re ((f . (x0 + (y * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:48
.= Re (((diff f,z0) * ((x0 + (y * )) - (x0 + (y0 * )))) + (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A18, A43, A45
.= (Re ((diff f,z0) * ((x0 + (y * )) - (x0 + (y0 * ))))) + (Re (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by COMPLEX1:19
.= (((Re (diff f,z0)) * (x0 - x0)) - ((Im (diff f,z0)) * (y - y0))) + (Re (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A39
.= (- ((Im (diff f,z0)) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * ))) by a2, A41, COMSEQ_3:def 3 ;
hence (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff f,z0)) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * ))) ; :: thesis:

end;

A47: 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:
assume A48: y in Ny0 ; :: thesis:
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 A40, A48
.= (LD3 . (y - y0)) + ((Re R) . ((x0 - x0) + ((y - y0) * ))) by A11
.= (LD3 . (y - y0)) + (R2 . (y - y0)) by A26 ; :: thesis:

end;

A49: 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:
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 A38
.= ((Im (diff f,z0)) * (x - x0)) + ((Re (diff f,z0)) * (y - y0)) by COMPLEX1:28 ; :: thesis:

end;

A50: 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:
(x0 + (y * )) - (x0 + (y0 * )) in dom R by A25, XCMPLX_0:def 2;
then A51: (y - y0) * in dom (Im R) by COMSEQ_3:def 4;
assume y in Ny0 ; :: thesis:
then A53: x0 + (y * ) in N by A36;
then x0 + (y * ) in dom f by A12;
then A54: x0 + (y * ) in dom (Im f) by COMSEQ_3:def 4;
A55: x0 + (y0 * ) in N by A3, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A12;
then A56: x0 + (y0 * ) in dom (Im f) by COMSEQ_3:def 4;
(x0 + (y * )) - (x0 + (y0 * )) in COMPLEX by XCMPLX_0:def 2;
then a3: R . ((x0 + (y * )) - (x0 + (y0 * ))) = R /. ((x0 + (y * )) - (x0 + (y0 * ))) by b2, PARTFUN1:def 8;
(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Im f) . (x0 + (y * ))) - (v . <*x0,y0*>) by A2, A12, A53
.= ((Im f) . (x0 + (y * ))) - ((Im f) . (x0 + (y0 * ))) by A2, A12, A55
.= (Im (f . (x0 + (y * )))) - ((Im f) . (x0 + (y0 * ))) by A54, COMSEQ_3:def 4
.= (Im (f . (x0 + (y * )))) - (Im (f . (x0 + (y0 * )))) by A56, COMSEQ_3:def 4
.= Im ((f . (x0 + (y * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:48
.= Im (((diff f,z0) * ((x0 + (y * )) - (x0 + (y0 * )))) + (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A18, A53, A55
.= (Im ((diff f,z0) * ((x0 + (y * )) - (x0 + (y0 * ))))) + (Im (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by COMPLEX1:19
.= (((Im (diff f,z0)) * (x0 - x0)) + ((Re (diff f,z0)) * (y - y0))) + (Im (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A49
.= ((Re (diff f,z0)) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * ))) by a3, A51, COMSEQ_3:def 4 ;
hence (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff f,z0)) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * ))) ; :: thesis:

end;

A57: 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:
assume A58: y in Ny0 ; :: thesis:
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 A50, A58
.= (LD1 . (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * ))) by A7
.= (LD1 . (y - y0)) + (R4 . (y - y0)) by A15 ; :: thesis:

end;

now

let s be set ; :: thesis:
assume s in (reproj 2,xy0) .: Ny0 ; :: thesis:
then consider y being Element of REAL such that
A59: y in Ny0 and
A60: s = (reproj 2,xy0) . y by FUNCT_2:116;
A61: x0 + (y * ) in N by A36, A59;
s = Replace xy0,2,y by A60, PDIFF_1:def 5
.= <*x0,y*> by A4, FINSEQ_7:16 ;
hence s in dom v by A2, A12, A61; :: thesis:

end;

then ( dom (reproj 2,xy0) = REAL & (reproj 2,xy0) .: Ny0 c= dom v ) by FUNCT_2:def 1, TARSKI:def 3;
then A62: Ny0 c= dom (v * (reproj 2,xy0)) by FUNCT_3:3;
then A63: v * (reproj 2,xy0) is_differentiable_in (proj 2,2) . xy0 by A10, A57, FDIFF_1:def 5;
A64: for x being Real holds (v * (reproj 1,xy0)) . x = v . <*x,y0*>

proof

let x be Real; :: thesis:
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:23
.= v . (Replace xy0,1,x) by PDIFF_1:def 5
.= v . <*x,y0*> by A4, FINSEQ_7:15 ;
:: thesis:

end;

now

let s be set ; :: thesis:
assume s in (reproj 2,xy0) .: Ny0 ; :: thesis:
then consider y being Element of REAL such that
A65: y in Ny0 and
A66: s = (reproj 2,xy0) . y by FUNCT_2:116;
A67: x0 + (y * ) in N by A36, A65;
s = Replace xy0,2,y by A66, PDIFF_1:def 5
.= <*x0,y*> by A4, FINSEQ_7:16 ;
hence s in dom u by A1, A12, A67; :: thesis:

end;

then ( dom (reproj 2,xy0) = REAL & (reproj 2,xy0) .: Ny0 c= dom u ) by FUNCT_2:def 1, TARSKI:def 3;
then A68: Ny0 c= dom (u * (reproj 2,xy0)) by FUNCT_3:3;
then A69: u * (reproj 2,xy0) is_differentiable_in (proj 2,2) . xy0 by A10, A47, FDIFF_1:def 5;
LD3 . 1 = - ((Im (diff f,z0)) * 1) by A11
.= - (Im (diff f,z0)) ;
then A70: partdiff u,xy0,2 = - (Im (diff f,z0)) by A10, A47, A68, A69, FDIFF_1:def 6;
A71: LD1 . 1 = (Re (diff f,z0)) * 1 by A7
.= Re (diff f,z0) ;
A72: (proj 1,2) . xy0 = xy0 . 1 by PDIFF_1:def 1
.= x0 by A4, FINSEQ_1:61 ;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by A34, RCOMP_1:def 7;
deffunc H₆( Real) -> Element of REAL = (Im R) . $1;
consider R3 being Function of REAL ,REAL such that
A73: for y being Real holds R3 . y = H₆(y) from FUNCT_2:sch 4();
A74: for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R3 /* h) is convergent & lim ((h " ) (#) (R3 /* h)) = 0 )

proof

let h be convergent_to_0 Real_Sequence; :: thesis:
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz = h as Complex_Sequence by FUNCT_2:8;
reconsider hz = hz as convergent_to_0 Complex_Sequence by Lm4;

now

d2: dom R = COMPLEX by PARTFUN1:def 4;
then A75: rng hz c= dom R ;
let n be Element of NAT ; :: thesis:
A76: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
A77: dom R3 = REAL by PARTFUN1:def 4;
then A78: rng h c= dom R3 ;
dom R3 c= dom (Im R) by A77, Th1, NUMBERS:11;
then A79: h . n in dom (Im R) by A77, TARSKI:def 3;
h . n in COMPLEX by XCMPLX_0:def 2;
then d1: R /. (h . n) = R . (h . n) by d2, PARTFUN1:def 8;
thus ((h " ) (#) (R3 /* h)) . n = ((h " ) . n) * ((R3 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R3 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R3 . (h . n)) by A78, FUNCT_2:185
.= ((h . n) " ) * ((Im R) . (h . n)) by A73
.= ((Re ((h . n) " )) * (Im (R /. (h . n)))) + ((Re (R /. (h . n))) * (Im ((h . n) " ))) by d1, A79, A76, COMSEQ_3:def 4
.= Im (((h . n) " ) * (R /. (h . n))) by COMPLEX1:24
.= Im (((hz " ) . n) * (R /. (hz . n))) by VALUED_1:10
.= Im (((hz " ) . n) * ((R /* hz) . n)) by A75, FUNCT_2:186
.= Im (((hz " ) (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis:

end;

then A80: (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 A80, COMPLEX1:12, COMSEQ_3:41; :: thesis:

end;

deffunc H₇( Real) -> Element of REAL = (Re R) . $1;
consider R1 being Function of REAL ,REAL such that
A81: for x being Real holds R1 . x = H₇(x) from FUNCT_2:sch 4();
reconsider R3 = R3 as REST by A74, FDIFF_1:def 3;
A82: for x being Real st x in Nx0 holds
x + (y0 * ) in N

proof

let x be Real; :: thesis:
assume x in Nx0 ; :: thesis:
then |.(x - x0).| < r0 by RCOMP_1:8;
then ( x + (y0 * ) is Complex & |.((x + (y0 * )) - z0).| < r0 ) by A3, XCMPLX_0:def 2;
then x + (y0 * ) in { y where y is Complex : |.(y - z0).| < r0 } ;
hence x + (y0 * ) in N by A35; :: thesis:

end;

A83: 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 + (y0 * )) - (x0 + (y0 * )) in dom R by A25, XCMPLX_0:def 2;
then A84: x - x0 in dom (Im R) by COMSEQ_3:def 4;
assume x in Nx0 ; :: thesis:
then A86: x + (y0 * ) in N by A82;
then x + (y0 * ) in dom f by A12;
then A87: x + (y0 * ) in dom (Im f) by COMSEQ_3:def 4;
A88: x0 + (y0 * ) in N by A3, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A12;
then A89: x0 + (y0 * ) in dom (Im f) by COMSEQ_3:def 4;
(x + (y0 * )) - (x0 + (y0 * )) in COMPLEX by XCMPLX_0:def 2;
then a4: R . ((x + (y0 * )) - (x0 + (y0 * ))) = R /. ((x + (y0 * )) - (x0 + (y0 * ))) by b2, PARTFUN1:def 8;
(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im f) . (x + (y0 * ))) - (v . <*x0,y0*>) by A2, A12, A86
.= ((Im f) . (x + (y0 * ))) - ((Im f) . (x0 + (y0 * ))) by A2, A12, A88
.= (Im (f . (x + (y0 * )))) - ((Im f) . (x0 + (y0 * ))) by A87, COMSEQ_3:def 4
.= (Im (f . (x + (y0 * )))) - (Im (f . (x0 + (y0 * )))) by A89, COMSEQ_3:def 4
.= Im ((f . (x + (y0 * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:48
.= Im (((diff f,z0) * ((x + (y0 * )) - (x0 + (y0 * )))) + (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A18, A86, A88
.= (Im ((diff f,z0) * ((x + (y0 * )) - (x0 + (y0 * ))))) + (Im (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by COMPLEX1:19
.= (((Im (diff f,z0)) * (x - x0)) + ((Re (diff f,z0)) * (y0 - y0))) + (Im (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A49
.= ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by a4, A84, COMSEQ_3:def 4 ;
hence (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) ; :: thesis:

end;

A90: 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:
assume A91: x in Nx0 ; :: thesis:
thus ((v * (reproj 1,xy0)) . x) - ((v * (reproj 1,xy0)) . x0) = (v . <*x,y0*>) - ((v * (reproj 1,xy0)) . x0) by A64
.= (v . <*x,y0*>) - (v . <*x0,y0*>) by A64
.= ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A83, A91
.= (LD2 . (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A6
.= (LD2 . (x - x0)) + (R3 . (x - x0)) by A73 ; :: thesis:

end;

for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 )

proof

now

dom R = COMPLEX by PARTFUN1:def 4;
then A92: rng hz c= dom R ;
let n be Element of NAT ; :: thesis:
A93: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
A94: dom R1 = REAL by PARTFUN1:def 4;
then A95: rng h c= dom R1 ;
dom R1 c= dom (Re R) by A94, Th1, NUMBERS:11;
then A96: h . n in dom (Re R) by A94, TARSKI:def 3;
thus ((h " ) (#) (R1 /* h)) . n = ((h " ) . n) * ((R1 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R1 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R1 /. (h . n)) by A95, FUNCT_2:186
.= ((h . n) " ) * ((Re R) . (h . n)) by A81
.= ((Re ((h . n) " )) * (Re (R . (h . n)))) - ((Im ((h . n) " )) * (Im (R . (h . n)))) by A96, A93, COMSEQ_3:def 3
.= Re (((h . n) " ) * (R . (h . n))) by COMPLEX1:24
.= Re (((hz " ) . n) * (R /. (hz . n))) by VALUED_1:10
.= Re (((hz " ) . n) * ((R /* hz) . n)) by A92, FUNCT_2:186
.= Re (((hz " ) (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis:

end;

then A97: (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 A97, COMPLEX1:12, COMSEQ_3:41; :: thesis:

end;

then reconsider R1 = R1 as REST by FDIFF_1:def 3;
A98: LD2 . 1 = (Im (diff f,z0)) * 1 by A6
.= Im (diff f,z0) ;
A99: for x being Real holds (u * (reproj 1,xy0)) . x = u . <*x,y0*>

proof

let x be Real; :: thesis:
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:23
.= u . (Replace xy0,1,x) by PDIFF_1:def 5
.= u . <*x,y0*> by A4, FINSEQ_7:15 ;
:: thesis:

end;

A100: 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 + (y0 * )) - (x0 + (y0 * )) in dom R by A25, XCMPLX_0:def 2;
then A101: x - x0 in dom (Re R) by COMSEQ_3:def 3;
assume x in Nx0 ; :: thesis:
then A103: x + (y0 * ) in N by A82;
then x + (y0 * ) in dom f by A12;
then A104: x + (y0 * ) in dom (Re f) by COMSEQ_3:def 3;
A105: x0 + (y0 * ) in N by A3, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A12;
then A106: x0 + (y0 * ) in dom (Re f) by COMSEQ_3:def 3;
(x + (y0 * )) - (x0 + (y0 * )) in COMPLEX by XCMPLX_0:def 2;
then a5: R . ((x + (y0 * )) - (x0 + (y0 * ))) = R /. ((x + (y0 * )) - (x0 + (y0 * ))) by b2, PARTFUN1:def 8;
(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re f) . (x + (y0 * ))) - (u . <*x0,y0*>) by A1, A12, A103
.= ((Re f) . (x + (y0 * ))) - ((Re f) . (x0 + (y0 * ))) by A1, A12, A105
.= (Re (f . (x + (y0 * )))) - ((Re f) . (x0 + (y0 * ))) by A104, COMSEQ_3:def 3
.= (Re (f . (x + (y0 * )))) - (Re (f . (x0 + (y0 * )))) by A106, COMSEQ_3:def 3
.= Re ((f . (x + (y0 * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:48
.= Re (((diff f,z0) * ((x + (y0 * )) - (x0 + (y0 * )))) + (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A18, A103, A105
.= (Re ((diff f,z0) * ((x + (y0 * )) - (x0 + (y0 * ))))) + (Re (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by COMPLEX1:19
.= (((Re (diff f,z0)) * (x - x0)) - ((Im (diff f,z0)) * (y0 - y0))) + (Re (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A39
.= ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by a5, A101, COMSEQ_3:def 3 ;
hence (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) ; :: thesis:

end;

A107: 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:
assume A108: x in Nx0 ; :: thesis:
thus ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (u . <*x,y0*>) - ((u * (reproj 1,xy0)) . x0) by A99
.= (u . <*x,y0*>) - (u . <*x0,y0*>) by A99
.= ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A100, A108
.= (LD1 . (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A7
.= (LD1 . (x - x0)) + (R1 . (x - x0)) by A81 ; :: thesis:

end;

now

let s be set ; :: thesis:
assume s in (reproj 1,xy0) .: Nx0 ; :: thesis:
then consider x being Element of REAL such that
A109: x in Nx0 and
A110: s = (reproj 1,xy0) . x by FUNCT_2:116;
A111: x + (y0 * ) in N by A82, A109;
s = Replace xy0,1,x by A110, PDIFF_1:def 5
.= <*x,y0*> by A4, FINSEQ_7:15 ;
hence s in dom v by A2, A12, A111; :: thesis:

end;

then ( dom (reproj 1,xy0) = REAL & (reproj 1,xy0) .: Nx0 c= dom v ) by FUNCT_2:def 1, TARSKI:def 3;
then A112: Nx0 c= dom (v * (reproj 1,xy0)) by FUNCT_3:3;
then A113: v * (reproj 1,xy0) is_differentiable_in (proj 1,2) . xy0 by A72, A90, FDIFF_1:def 5;

now

let s be set ; :: thesis:
assume s in (reproj 1,xy0) .: Nx0 ; :: thesis:
then consider x being Element of REAL such that
A114: x in Nx0 and
A115: s = (reproj 1,xy0) . x by FUNCT_2:116;
A116: x + (y0 * ) in N by A82, A114;
s = Replace xy0,1,x by A115, PDIFF_1:def 5
.= <*x,y0*> by A4, FINSEQ_7:15 ;
hence s in dom u by A1, A12, A116; :: thesis:

end;

then ( dom (reproj 1,xy0) = REAL & (reproj 1,xy0) .: Nx0 c= dom u ) by FUNCT_2:def 1, TARSKI:def 3;
then A117: Nx0 c= dom (u * (reproj 1,xy0)) by FUNCT_3:3;
then u * (reproj 1,xy0) is_differentiable_in (proj 1,2) . xy0 by A72, A107, FDIFF_1:def 5;
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 A72, A10, A107, A90, A57, A117, A69, A70, A98, A112, A113, A71, A62, A63, FDIFF_1:def 6, PDIFF_1:def 11; :: thesis: