let f be PartFunc of COMPLEX,COMPLEX; :: thesis:
let u, v be PartFunc of (REAL 2),REAL; :: thesis:
let z0 be Complex; :: thesis:
let x00, y00 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 = x00 + (y00 * ) and
A4: xy0 = <*x00,y00*> and
A5: f is_differentiable_in z0 ; :: thesis:
reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;
A6: z0 = x0 + (y0 * ) by A3;
A7: xy0 = <*x0,y0*> by A4;
deffunc H₁( Real) -> Element of REAL = In (((Im (diff (f,z0))) * $1),REAL);
consider LD2 being Function of REAL,REAL such that
A8: for x being Element of REAL holds LD2 . x = H₁(x) from FUNCT_2:sch 4();
A9: for x being Real holds LD2 . x = (Im (diff (f,z0))) * x

let x be Real; :: thesis:
reconsider x = x as Element of REAL by XREAL_0:def 1;
LD2 . x = H₁(x) by A8;
hence LD2 . x = (Im (diff (f,z0))) * x ; :: thesis:

end;

reconsider LD2 = LD2 as LinearFunc by A9, FDIFF_1:def 3;
deffunc H₂( Real) -> Element of REAL = In (((Re (diff (f,z0))) * $1),REAL);
consider LD1 being Function of REAL,REAL such that
A10: for x being Element of REAL holds LD1 . x = H₂(x) from FUNCT_2:sch 4();
A11: for x being Real holds LD1 . x = (Re (diff (f,z0))) * x

proof

let x be Real; :: thesis:
reconsider x = x as Element of REAL by XREAL_0:def 1;
LD1 . x = H₂(x) by A10;
hence LD1 . x = (Re (diff (f,z0))) * x ; :: thesis:

end;

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

proof

let y be Real; :: thesis:
reconsider yy = y, dwa = 2 as Element of REAL by XREAL_0:def 1;
yy in REAL ;
then yy in dom (reproj (2,xy0)) by PDIFF_1:def 5;
hence (v * (reproj (2,xy0))) . y = v . ((reproj (2,xy0)) . y) by FUNCT_1:13
.= v . (Replace (xy0,2,yy)) by PDIFF_1:def 5
.= v . <*x0,yy*> by A7, FINSEQ_7:14
.= v . <*x0,y*> ;
:: thesis:

end;

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

proof

let y be Real; :: thesis:
reconsider yy = y as Element of REAL by XREAL_0:def 1;
y in REAL by XREAL_0:def 1;
then y in dom (reproj (2,xy0)) by PDIFF_1:def 5;
hence (u * (reproj (2,xy0))) . y = u . ((reproj (2,xy0)) . y) by FUNCT_1:13
.= u . (Replace (xy0,2,yy)) by PDIFF_1:def 5
.= u . <*x0,y*> by A7, FINSEQ_7:14 ;
:: thesis:

end;

A14: (proj (2,2)) . xy0 = xy0 . 2 by PDIFF_1:def 1
.= y0 by A7, FINSEQ_1:44 ;
reconsider LD1 = LD1 as LinearFunc by A11, FDIFF_1:def 3;
deffunc H₃( Real) -> Element of REAL = In ((- ((Im (diff (f,z0))) * $1)),REAL);
consider LD3 being Function of REAL,REAL such that
A15: for x being Element of REAL holds LD3 . x = H₃(x) from FUNCT_2:sch 4();
A16: for x being Real holds LD3 . x = - ((Im (diff (f,z0))) * x)

proof

let x be Real; :: thesis:
reconsider x = x as Element of REAL by XREAL_0:def 1;
LD3 . x = H₃(x) by A15;
hence LD3 . x = - ((Im (diff (f,z0))) * x) ; :: thesis:

end;

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 A16
.= (- (Im (diff (f,z0)))) * x ; :: thesis:

end;

then reconsider LD3 = LD3 as LinearFunc by FDIFF_1:def 3;
reconsider z0 = z0 as Element of COMPLEX by XCMPLX_0:def 2;
consider N being Neighbourhood of z0 such that
A17: N c= dom f and
A18: ex L being C_LinearFunc ex R being C_RestFunc 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_LinearFunc, R being C_RestFunc such that
A19: ( 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 A18;
deffunc H₄( Real) -> Element of REAL = In (((Im R) . ($1 * )),REAL);
consider R4 being Function of REAL,REAL such that
A20: for y being Element of REAL holds R4 . y = H₄(y) from FUNCT_2:sch 4();
A21: 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 A22: z in N ; :: thesis:
reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
consider a0 being Complex such that
A23: for w being Complex holds L /. w = a0 * w by CFDIFF_1:def 4;
L /. (1r * (z - z0)) = (a0 * 1r) * (z - z0) by A23
.= (L /. 1r) * (z - z0) by A23 ;
hence (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0)) by A19, A22; :: thesis:

end;

A24: 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 A25: ( x + (y * ) in N & x0 + (y0 * ) in N ) ; :: thesis:
then ( f . (x + (y * )) = f /. (x + (y * )) & f . (x0 + (y0 * )) = f /. (x0 + (y0 * )) ) by A17, PARTFUN1:def 6;
hence (f . (x + (y * ))) - (f . (x0 + (y0 * ))) = ((diff (f,z0)) * ((x + (y * )) - (x0 + (y0 * )))) + (R /. ((x + (y * )) - (x0 + (y0 * )))) by A21, A25, A6; :: thesis:

end;

A26: dom R = COMPLEX by PARTFUN1:def 2;
for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis:
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz0 = h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 = hz0 as non-zero 0 -convergent Complex_Sequence by Lm3;
set hz = (#) hz0;
reconsider hz = (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;

now :: thesis:

A27: rng hz c= dom R by A26;
dom R4 = REAL by PARTFUN1:def 2;
then A28: rng h c= dom R4 ;
let n be Nat; :: thesis:
A29: n in NAT by ORDINAL1:def 12;
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A30: ( Im ((h . nn) ") = 0 & Re ((h . nn) ") = (h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;
A31: hz . n = (h . n) * by VALUED_1:6;
reconsider hn = h . n as Real ;
(h . n) * in COMPLEX by XCMPLX_0:def 2;
then A32: (h . n) * in dom (Im R) by Th1;
thus ((h ") (#) (R4 /* h)) . n = ((h ") . n) * ((R4 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R4 /* h) . n) by VALUED_1:10
.= ((h . n) ") * (R4 . hn) by A28, FUNCT_2:108, A29
.= ((h . nn) ") * H₄(hn) by A20
.= ((h . n) ") * ((Im R) . ((h . n) * ))
.= ((Re ((h . n) ")) * (Im (R . ((h . n) * )))) + ((Re (R . ((h . n) * ))) * (Im ((h . n) "))) by A32, A30, COMSEQ_3:def 4
.= Im ((((hz . n) / ) ") * (R . (hz . n))) by A31, COMPLEX1:9
.= Im (( / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213
.= Im (( * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10
.= Im ( * (((hz ") . n) * (R . (hz . n))))
.= ((Re ) * (Im (((hz ") . n) * (R /. (hz . n))))) + ((Re (((hz ") . n) * (R /. (hz . n)))) * (Im )) by COMPLEX1:9
.= Re (((hz ") . n) * ((R /* hz) . n)) by A27, COMPLEX1:7, FUNCT_2:109, A29
.= Re (((hz ") (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis:

end;

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

end;

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

proof

now :: thesis:

dom R2 = REAL by PARTFUN1:def 2;
then A38: rng h c= dom R2 ;
let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A39: ( Im ((h . nn) ") = 0 & Re ((h . nn) ") = (h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;
A40: hz . n = (h . n) * by VALUED_1:6;
dom (Re R) = COMPLEX by Th1;
then A41: (h . n) * in dom (Re R) by XCMPLX_0:def 2;
A42: R . (hz . n) = R /. (hz . n) ;
reconsider hn = h . n as Real ;
thus ((h ") (#) (R2 /* h)) . n = ((h ") . n) * ((R2 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R2 /* h) . n) by VALUED_1:10
.= ((h . nn) ") * (R2 . (h . n)) by A38, FUNCT_2:108
.= ((h . nn) ") * H₅(hn) by A35
.= ((h . n) ") * ((Re R) . ((h . n) * ))
.= ((Re ((h . n) ")) * (Re (R . ((h . n) * )))) - ((Im ((h . n) ")) * (Im (R . ((h . n) * )))) by A41, A39, COMSEQ_3:def 3
.= Re ((((hz . n) / ) ") * (R . (hz . n))) by A40, COMPLEX1:9
.= Re (( / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213
.= Re (( * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10
.= Re ( * (((hz ") . n) * (R . (hz . n))))
.= ((Re ) * (Re (((hz ") . n) * (R . (hz . n))))) - ((Im ) * (Im (((hz ") . n) * (R . (hz . n))))) by COMPLEX1:9
.= - (Im (((hz ") . nn) * ((R /* hz) . nn))) by A42, A37, COMPLEX1:7, FUNCT_2:109
.= - (Im (((hz ") (#) (R /* hz)) . n)) by VALUED_1:5
.= - ((Im ((hz ") (#) (R /* hz))) . n) by COMSEQ_3:def 6 ; :: thesis:

end;

then A43: (h ") (#) (R2 /* h) = - (Im ((hz ") (#) (R /* hz))) by SEQ_1:10;
lim ((hz ") (#) (R /* hz)) = 0 by CFDIFF_1:def 3;
then lim (Im ((hz ") (#) (R /* hz))) = Im 0 by A36, COMSEQ_3:41;
then lim ((h ") (#) (R2 /* h)) = - (Im 0) by A43, A36, SEQ_2:10
.= 0 by COMPLEX1:4 ;
hence ( (h ") (#) (R2 /* h) is convergent & lim ((h ") (#) (R2 /* h)) = 0 ) by A43, A36, SEQ_2:9; :: thesis:

end;

then reconsider R2 = R2 as RestFunc by FDIFF_1:def 2;
consider r0 being Real such that
A44: 0 < r0 and
A45: { 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 A44, RCOMP_1:def 6;
A46: 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 A6;
then A47: |.((x0 + (y * )) - z0).| = |.(y - y0).| * |..| by COMPLEX1:65;
assume y in Ny0 ; :: thesis:
then ( x0 + (y * ) is Complex & |.((x0 + (y * )) - z0).| < r0 ) by A47, COMPLEX1:49, RCOMP_1:1;
then x0 + (y * ) in { w where w is Complex : |.(w - z0).| < r0 } ;
hence x0 + (y * ) in N by A45; :: thesis:

end;

A48: 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:13
.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * ) ; :: thesis:

end;

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

end;

A50: 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 A34, XCMPLX_0:def 2;
then A51: (y - y0) * in dom (Re R) by COMSEQ_3:def 3;
assume y in Ny0 ; :: thesis:
then A52: x0 + (y * ) in N by A46;
then x0 + (y * ) in dom f by A17;
then A53: x0 + (y * ) in dom (Re f) by COMSEQ_3:def 3;
A54: x0 + (y0 * ) in N by A6, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A17;
then A55: x0 + (y0 * ) in dom (Re f) by COMSEQ_3:def 3;
(u . <*x0,y*>) - (u . <*x0,y0*>) = ((Re f) . (x0 + (y * ))) - (u . <*x0,y0*>) by A1, A17, A52
.= ((Re f) . (x0 + (y * ))) - ((Re f) . (x0 + (y0 * ))) by A1, A17, A54
.= (Re (f . (x0 + (y * )))) - ((Re f) . (x0 + (y0 * ))) by A53, COMSEQ_3:def 3
.= (Re (f . (x0 + (y * )))) - (Re (f . (x0 + (y0 * )))) by A55, COMSEQ_3:def 3
.= Re ((f . (x0 + (y * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:19
.= Re (((diff (f,z0)) * ((x0 + (y * )) - (x0 + (y0 * )))) + (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A24, A52, A54
.= (Re ((diff (f,z0)) * ((x0 + (y * )) - (x0 + (y0 * ))))) + (Re (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by COMPLEX1:8
.= (((Re (diff (f,z0))) * (x0 - x0)) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A49
.= (((Re (diff (f,z0))) * 0) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * )) - (x0 + (y0 * )))))
.= (- ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * )) - (x0 + (y0 * )))))
.= (- ((Im (diff (f,z0))) * (y - y0))) + (Re (R . ((x0 + (y * )) - (x0 + (y0 * )))))
.= (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * ))) by A51, 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;

A56: 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 A57: y in Ny0 ; :: thesis:
reconsider yy0 = y - y0 as Element of REAL by XREAL_0:def 1;
thus ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (u . <*x0,y*>) - ((u * (reproj (2,xy0))) . y0) by A13
.= (u . <*x0,y*>) - (u . <*x0,y0*>) by A13
.= (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * ))) by A50, A57
.= (LD3 . (y - y0)) + ((Re R) . ((x0 - x0) + ((y - y0) * ))) by A16
.= (LD3 . (y - y0)) + H₅(yy0)
.= (LD3 . (y - y0)) + (R2 . (y - y0)) by A35 ; :: thesis:

end;

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

end;

A59: 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 A34, XCMPLX_0:def 2;
then A60: (y - y0) * in dom (Im R) by COMSEQ_3:def 4;
assume y in Ny0 ; :: thesis:
then A61: x0 + (y * ) in N by A46;
then x0 + (y * ) in dom f by A17;
then A62: x0 + (y * ) in dom (Im f) by COMSEQ_3:def 4;
A63: x0 + (y0 * ) in N by A6, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A17;
then A64: x0 + (y0 * ) in dom (Im f) by COMSEQ_3:def 4;
(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Im f) . (x0 + (y * ))) - (v . <*x0,y0*>) by A2, A17, A61
.= ((Im f) . (x0 + (y * ))) - ((Im f) . (x0 + (y0 * ))) by A2, A17, A63
.= (Im (f . (x0 + (y * )))) - ((Im f) . (x0 + (y0 * ))) by A62, COMSEQ_3:def 4
.= (Im (f . (x0 + (y * )))) - (Im (f . (x0 + (y0 * )))) by A64, COMSEQ_3:def 4
.= Im ((f . (x0 + (y * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:19
.= Im (((diff (f,z0)) * ((x0 + (y * )) - (x0 + (y0 * )))) + (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A24, A61, A63
.= (Im ((diff (f,z0)) * ((x0 + (y * )) - (x0 + (y0 * ))))) + (Im (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by COMPLEX1:8
.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R /. ((x0 + (y * )) - (x0 + (y0 * ))))) by A58
.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R . ((x0 + (y * )) - (x0 + (y0 * )))))
.= ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * ))) by A60, 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;

A65: 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 A66: y in Ny0 ; :: thesis:
reconsider yy0 = y - y0 as Element of REAL by XREAL_0:def 1;
thus ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (v . <*x0,y*>) - ((v * (reproj (2,xy0))) . y0) by A12
.= (v . <*x0,y*>) - (v . <*x0,y0*>) by A12
.= ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * ))) by A59, A66
.= (LD1 . (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * ))) by A11
.= (LD1 . (y - y0)) + H₄(yy0)
.= (LD1 . (y - y0)) + (R4 . (y - y0)) by A20 ; :: thesis:

end;

now :: thesis:

let s be object ; :: thesis:
assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis:
then consider y being Element of REAL such that
A67: y in Ny0 and
A68: s = (reproj (2,xy0)) . y by FUNCT_2:65;
A69: x0 + (y * ) in N by A46, A67;
s = Replace (xy0,2,y) by A68, PDIFF_1:def 5
.= <*x0,y*> by A7, FINSEQ_7:14 ;
hence s in dom v by A2, A17, A69; :: thesis:

end;

then ( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom v ) by FUNCT_2:def 1, TARSKI:def 3;
then A70: Ny0 c= dom (v * (reproj (2,xy0))) by FUNCT_3:3;
then A71: v * (reproj (2,xy0)) is_differentiable_in (proj (2,2)) . xy0 by A14, A65, FDIFF_1:def 4;
A72: for x being Element of REAL holds (v * (reproj (1,xy0))) . x = v . <*x,y0*>

proof

let x be Element of 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:13
.= v . (Replace (xy0,1,x)) by PDIFF_1:def 5
.= v . <*x,y0*> by A7, FINSEQ_7:13 ;
:: thesis:

end;

now :: thesis:

let s be object ; :: thesis:
assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis:
then consider y being Element of REAL such that
A73: y in Ny0 and
A74: s = (reproj (2,xy0)) . y by FUNCT_2:65;
A75: x0 + (y * ) in N by A46, A73;
s = Replace (xy0,2,y) by A74, PDIFF_1:def 5
.= <*x0,y*> by A7, FINSEQ_7:14 ;
hence s in dom u by A1, A17, A75; :: thesis:

end;

then ( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom u ) by FUNCT_2:def 1, TARSKI:def 3;
then A76: Ny0 c= dom (u * (reproj (2,xy0))) by FUNCT_3:3;
then A77: u * (reproj (2,xy0)) is_differentiable_in (proj (2,2)) . xy0 by A14, A56, FDIFF_1:def 4;
LD3 . 1 = - ((Im (diff (f,z0))) * 1) by A16
.= - (Im (diff (f,z0))) ;
then A78: partdiff (u,xy0,2) = - (Im (diff (f,z0))) by A14, A56, A76, A77, FDIFF_1:def 5;
A79: LD1 . 1 = (Re (diff (f,z0))) * 1 by A11
.= Re (diff (f,z0)) ;
A80: (proj (1,2)) . xy0 = xy0 . 1 by PDIFF_1:def 1
.= x0 by A7, FINSEQ_1:44 ;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by A44, RCOMP_1:def 6;
deffunc H₆( Real) -> Element of REAL = In (((Im R) . $1),REAL);
consider R3 being Function of REAL,REAL such that
A81: for y being Element of REAL holds R3 . y = H₆(y) from FUNCT_2:sch 4();
A82: for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )

proof

let h be non-zero 0 -convergent Real_Sequence; :: thesis:
rng h c= COMPLEX by NUMBERS:11, XBOOLE_1:1;
then reconsider hz = h as Complex_Sequence by FUNCT_2:6;
reconsider hz = hz as non-zero 0 -convergent Complex_Sequence by Lm3;

now :: thesis:

dom R = COMPLEX by PARTFUN1:def 2;
then A83: rng hz c= dom R ;
let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A84: ( Im ((h . nn) ") = 0 & Re ((h . nn) ") = (h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;
A85: dom R3 = REAL by PARTFUN1:def 2;
then A86: rng h c= dom R3 ;
dom R3 c= dom (Im R) by A85, Th1, NUMBERS:11;
then A87: h . nn in dom (Im R) by A85, TARSKI:def 3;
thus ((h ") (#) (R3 /* h)) . n = ((h ") . n) * ((R3 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R3 /* h) . n) by VALUED_1:10
.= ((h . nn) ") * (R3 . (h . nn)) by A86, FUNCT_2:108
.= ((h . nn) ") * H₆(h . nn) by A81
.= ((h . n) ") * ((Im R) . (h . n))
.= ((Re ((h . n) ")) * (Im (R /. (h . n)))) + ((Re (R /. (h . n))) * (Im ((h . n) "))) by A87, A84, COMSEQ_3:def 4
.= Im (((h . n) ") * (R /. (h . n))) by COMPLEX1:9
.= Im (((hz ") . n) * (R /. (hz . n))) by VALUED_1:10
.= Im (((hz ") . nn) * ((R /* hz) . nn)) by A83, FUNCT_2:109
.= Im (((hz ") (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis:

end;

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

end;

deffunc H₇( Real) -> Element of REAL = In (((Re R) . $1),REAL);
consider R1 being Function of REAL,REAL such that
A89: for x being Element of REAL holds R1 . x = H₇(x) from FUNCT_2:sch 4();
reconsider R3 = R3 as RestFunc by A82, FDIFF_1:def 2;
A90: 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:1;
then ( x + (y0 * ) is Complex & |.((x + (y0 * )) - z0).| < r0 ) by A6;
then x + (y0 * ) in { y where y is Complex : |.(y - z0).| < r0 } ;
hence x + (y0 * ) in N by A45; :: thesis:

end;

A91: 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 A34, XCMPLX_0:def 2;
then A92: x - x0 in dom (Im R) by COMSEQ_3:def 4;
assume x in Nx0 ; :: thesis:
then A93: x + (y0 * ) in N by A90;
then x + (y0 * ) in dom f by A17;
then A94: x + (y0 * ) in dom (Im f) by COMSEQ_3:def 4;
A95: x0 + (y0 * ) in N by A6, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A17;
then A96: x0 + (y0 * ) in dom (Im f) by COMSEQ_3:def 4;
(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im f) . (x + (y0 * ))) - (v . <*x0,y0*>) by A2, A17, A93
.= ((Im f) . (x + (y0 * ))) - ((Im f) . (x0 + (y0 * ))) by A2, A17, A95
.= (Im (f . (x + (y0 * )))) - ((Im f) . (x0 + (y0 * ))) by A94, COMSEQ_3:def 4
.= (Im (f . (x + (y0 * )))) - (Im (f . (x0 + (y0 * )))) by A96, COMSEQ_3:def 4
.= Im ((f . (x + (y0 * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:19
.= Im (((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * )))) + (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A24, A93, A95
.= (Im ((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * ))))) + (Im (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by COMPLEX1:8
.= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A58
.= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R . ((x + (y0 * )) - (x0 + (y0 * )))))
.= ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A92, COMSEQ_3:def 4 ;
hence (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) ; :: thesis:

end;

A97: 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 A98: x in Nx0 ; :: thesis:
reconsider xx0 = x - x0 as Element of REAL by XREAL_0:def 1;
x in REAL by XREAL_0:def 1;
hence ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (v . <*x,y0*>) - ((v * (reproj (1,xy0))) . x0) by A72
.= (v . <*x,y0*>) - (v . <*x0,y0*>) by A72
.= ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A91, A98
.= (LD2 . (x - x0)) + ((Im R) . ((x - x0) + (0 * ))) by A9
.= (LD2 . (x - x0)) + H₆(xx0)
.= (LD2 . (x - x0)) + (R3 . xx0) by A81
.= (LD2 . (x - x0)) + (R3 . (x - x0)) ;
:: thesis:

end;

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

proof

now :: thesis:

dom R = COMPLEX by PARTFUN1:def 2;
then A99: rng hz c= dom R ;
let n be Nat; :: thesis:
reconsider nn = n as Element of NAT by ORDINAL1:def 12;
A100: ( Im ((h . nn) ") = 0 & Re ((h . nn) ") = (h . nn) " ) by COMPLEX1:def 1, COMPLEX1:def 2;
A101: dom R1 = REAL by PARTFUN1:def 2;
then A102: rng h c= dom R1 ;
dom R1 c= dom (Re R) by A101, Th1, NUMBERS:11;
then A103: h . nn in dom (Re R) by A101, TARSKI:def 3;
thus ((h ") (#) (R1 /* h)) . n = ((h ") . n) * ((R1 /* h) . n) by SEQ_1:8
.= ((h . n) ") * ((R1 /* h) . n) by VALUED_1:10
.= ((h . nn) ") * (R1 /. (h . nn)) by A102, FUNCT_2:109
.= ((h . nn) ") * H₇(h . nn) by A89
.= ((h . n) ") * ((Re R) . (h . n))
.= ((Re ((h . n) ")) * (Re (R . (h . n)))) - ((Im ((h . n) ")) * (Im (R . (h . n)))) by A103, A100, COMSEQ_3:def 3
.= Re (((h . n) ") * (R . (h . n))) by COMPLEX1:9
.= Re (((hz ") . n) * (R /. (hz . n))) by VALUED_1:10
.= Re (((hz ") . nn) * ((R /* hz) . nn)) by A99, FUNCT_2:109
.= Re (((hz ") (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis:

end;

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

end;

then reconsider R1 = R1 as RestFunc by FDIFF_1:def 2;
A105: LD2 . 1 = (Im (diff (f,z0))) * 1 by A9
.= Im (diff (f,z0)) ;
A106: for x being Element of REAL holds (u * (reproj (1,xy0))) . x = u . <*x,y0*>

proof

let x be Element of 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:13
.= u . (Replace (xy0,1,x)) by PDIFF_1:def 5
.= u . <*x,y0*> by A7, FINSEQ_7:13 ;
:: thesis:

end;

A107: 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 A34, XCMPLX_0:def 2;
then A108: x - x0 in dom (Re R) by COMSEQ_3:def 3;
assume x in Nx0 ; :: thesis:
then A109: x + (y0 * ) in N by A90;
then x + (y0 * ) in dom f by A17;
then A110: x + (y0 * ) in dom (Re f) by COMSEQ_3:def 3;
A111: x0 + (y0 * ) in N by A6, CFDIFF_1:7;
then x0 + (y0 * ) in dom f by A17;
then A112: x0 + (y0 * ) in dom (Re f) by COMSEQ_3:def 3;
(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re f) . (x + (y0 * ))) - (u . <*x0,y0*>) by A1, A17, A109
.= ((Re f) . (x + (y0 * ))) - ((Re f) . (x0 + (y0 * ))) by A1, A17, A111
.= (Re (f . (x + (y0 * )))) - ((Re f) . (x0 + (y0 * ))) by A110, COMSEQ_3:def 3
.= (Re (f . (x + (y0 * )))) - (Re (f . (x0 + (y0 * )))) by A112, COMSEQ_3:def 3
.= Re ((f . (x + (y0 * ))) - (f . (x0 + (y0 * )))) by COMPLEX1:19
.= Re (((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * )))) + (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A24, A109, A111
.= (Re ((diff (f,z0)) * ((x + (y0 * )) - (x0 + (y0 * ))))) + (Re (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by COMPLEX1:8
.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R /. ((x + (y0 * )) - (x0 + (y0 * ))))) by A49
.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R . ((x + (y0 * )) - (x0 + (y0 * )))))
.= ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A108, COMSEQ_3:def 3 ;
hence (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) ; :: thesis:

end;

A113: 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 A114: x in Nx0 ; :: thesis:
reconsider xx0 = x - x0 as Element of REAL by XREAL_0:def 1;
x in REAL by XREAL_0:def 1;
hence ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (u . <*x,y0*>) - ((u * (reproj (1,xy0))) . x0) by A106
.= (u . <*x,y0*>) - (u . <*x0,y0*>) by A106
.= ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A107, A114
.= (LD1 . (x - x0)) + ((Re R) . ((x - x0) + (0 * ))) by A11
.= (LD1 . (x - x0)) + H₇(xx0)
.= (LD1 . (x - x0)) + (R1 . xx0) by A89
.= (LD1 . (x - x0)) + (R1 . (x - x0)) ;
:: thesis:

end;

now :: thesis:

let s be object ; :: thesis:
assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis:
then consider x being Element of REAL such that
A115: x in Nx0 and
A116: s = (reproj (1,xy0)) . x by FUNCT_2:65;
A117: x + (y0 * ) in N by A90, A115;
s = Replace (xy0,1,x) by A116, PDIFF_1:def 5
.= <*x,y0*> by A7, FINSEQ_7:13 ;
hence s in dom v by A2, A17, A117; :: thesis:

end;

then ( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom v ) by FUNCT_2:def 1, TARSKI:def 3;
then A118: Nx0 c= dom (v * (reproj (1,xy0))) by FUNCT_3:3;
then A119: v * (reproj (1,xy0)) is_differentiable_in (proj (1,2)) . xy0 by A80, A97, FDIFF_1:def 4;

now :: thesis:

let s be object ; :: thesis:
assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis:
then consider x being Element of REAL such that
A120: x in Nx0 and
A121: s = (reproj (1,xy0)) . x by FUNCT_2:65;
A122: x + (y0 * ) in N by A90, A120;
s = Replace (xy0,1,x) by A121, PDIFF_1:def 5
.= <*x,y0*> by A7, FINSEQ_7:13 ;
hence s in dom u by A1, A17, A122; :: thesis:

end;

then ( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom u ) by FUNCT_2:def 1, TARSKI:def 3;
then A123: Nx0 c= dom (u * (reproj (1,xy0))) by FUNCT_3:3;
then u * (reproj (1,xy0)) is_differentiable_in (proj (1,2)) . xy0 by A80, A113, FDIFF_1:def 4;
hence ( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff (f,z0)) = partdiff (u,xy0,1) & Re (diff (f,z0)) = partdiff (v,xy0,2) & Im (diff (f,z0)) = - (partdiff (u,xy0,2)) & Im (diff (f,z0)) = partdiff (v,xy0,1) ) by A80, A14, A113, A97, A65, A123, A77, A78, A105, A118, A119, A79, A70, A71, FDIFF_1:def 5; :: thesis: