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 * <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*> & f is_differentiable_in z0 holds

( 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 * <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*> & f is_differentiable_in z0 holds

( 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 * <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*> & f is_differentiable_in z0 holds

( 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 x00, y00 be Real; :: thesis: for xy0 being Element of REAL 2 st ( 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 = x00 + (y00 * <i>) & xy0 = <*x00,y00*> & f is_differentiable_in z0 holds

( 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 * <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 = x00 + (y00 * <i>) & xy0 = <*x00,y00*> & f is_differentiable_in z0 implies ( 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 * <i>) in dom f holds

( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) and

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

A3: z0 = x00 + (y00 * <i>) and

A4: xy0 = <*x00,y00*> and

A5: f is_differentiable_in z0 ; :: thesis: ( 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) )

reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;

A6: z0 = x0 + (y0 * <i>) by A3;

A7: xy0 = <*x0,y0*> by A4;

deffunc H_{1}( 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_{1}(x)
from FUNCT_2:sch 4();

A9: for x being Real holds LD2 . x = (Im (diff (f,z0))) * x

deffunc H_{2}( 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_{2}(x)
from FUNCT_2:sch 4();

A11: for x being Real holds LD1 . x = (Re (diff (f,z0))) * x

.= y0 by A7, FINSEQ_1:44 ;

reconsider LD1 = LD1 as LinearFunc by A11, FDIFF_1:def 3;

deffunc H_{3}( 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_{3}(x)
from FUNCT_2:sch 4();

A16: for x being Real holds LD3 . x = - ((Im (diff (f,z0))) * x)

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_{4}( Real) -> Element of REAL = In (((Im R) . ($1 * <i>)),REAL);

consider R4 being Function of REAL,REAL such that

A20: for y being Element of REAL holds R4 . y = H_{4}(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))

(f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>))))

for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 )

deffunc H_{5}( Real) -> Element of REAL = In (((Re R) . ($1 * <i>)),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_{5}(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 )

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 * <i>) in N

(u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>)))

((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))

(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>)))

((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))

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

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_{6}( 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_{6}(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 )_{7}( 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_{7}(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 * <i>) in N

(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>)))

((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0))

( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )

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

(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>)))

((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))

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;

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

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 * <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*> & f is_differentiable_in z0 holds

( 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 * <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*> & f is_differentiable_in z0 holds

( 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 * <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*> & f is_differentiable_in z0 holds

( 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 x00, y00 be Real; :: thesis: for xy0 being Element of REAL 2 st ( 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 = x00 + (y00 * <i>) & xy0 = <*x00,y00*> & f is_differentiable_in z0 holds

( 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 * <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 = x00 + (y00 * <i>) & xy0 = <*x00,y00*> & f is_differentiable_in z0 implies ( 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 * <i>) in dom f holds

( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i>)) ) and

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

A3: z0 = x00 + (y00 * <i>) and

A4: xy0 = <*x00,y00*> and

A5: f is_differentiable_in z0 ; :: thesis: ( 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) )

reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;

A6: z0 = x0 + (y0 * <i>) by A3;

A7: xy0 = <*x0,y0*> by A4;

deffunc H

consider LD2 being Function of REAL,REAL such that

A8: for x being Element of REAL holds LD2 . x = H

A9: for x being Real holds LD2 . x = (Im (diff (f,z0))) * x

proof

reconsider LD2 = LD2 as LinearFunc by A9, FDIFF_1:def 3;
let x be Real; :: thesis: LD2 . x = (Im (diff (f,z0))) * x

reconsider x = x as Element of REAL by XREAL_0:def 1;

LD2 . x = H_{1}(x)
by A8;

hence LD2 . x = (Im (diff (f,z0))) * x ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

LD2 . x = H

hence LD2 . x = (Im (diff (f,z0))) * x ; :: thesis: verum

deffunc H

consider LD1 being Function of REAL,REAL such that

A10: for x being Element of REAL holds LD1 . x = H

A11: for x being Real holds LD1 . x = (Re (diff (f,z0))) * x

proof

A12:
for y being Real holds (v * (reproj (2,xy0))) . y = v . <*x0,y*>
let x be Real; :: thesis: LD1 . x = (Re (diff (f,z0))) * x

reconsider x = x as Element of REAL by XREAL_0:def 1;

LD1 . x = H_{2}(x)
by A10;

hence LD1 . x = (Re (diff (f,z0))) * x ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

LD1 . x = H

hence LD1 . x = (Re (diff (f,z0))) * x ; :: thesis: verum

proof

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

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

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

proof

A14: (proj (2,2)) . xy0 =
xy0 . 2
by PDIFF_1:def 1
let y be Real; :: thesis: (u * (reproj (2,xy0))) . y = u . <*x0,y*>

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

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

.= y0 by A7, FINSEQ_1:44 ;

reconsider LD1 = LD1 as LinearFunc by A11, FDIFF_1:def 3;

deffunc H

consider LD3 being Function of REAL,REAL such that

A15: for x being Element of REAL holds LD3 . x = H

A16: for x being Real holds LD3 . x = - ((Im (diff (f,z0))) * x)

proof

for x being Real holds LD3 . x = (- (Im (diff (f,z0)))) * x
let x be Real; :: thesis: LD3 . x = - ((Im (diff (f,z0))) * x)

reconsider x = x as Element of REAL by XREAL_0:def 1;

LD3 . x = H_{3}(x)
by A15;

hence LD3 . x = - ((Im (diff (f,z0))) * x) ; :: thesis: verum

end;reconsider x = x as Element of REAL by XREAL_0:def 1;

LD3 . x = H

hence LD3 . x = - ((Im (diff (f,z0))) * x) ; :: thesis: verum

proof

then reconsider LD3 = LD3 as LinearFunc by FDIFF_1:def 3;
let x be Real; :: thesis: LD3 . x = (- (Im (diff (f,z0)))) * x

thus LD3 . x = - ((Im (diff (f,z0))) * x) by A16

.= (- (Im (diff (f,z0)))) * x ; :: thesis: verum

end;thus LD3 . x = - ((Im (diff (f,z0))) * x) by A16

.= (- (Im (diff (f,z0)))) * x ; :: thesis: verum

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

consider R4 being Function of REAL,REAL such that

A20: for y being Element of REAL holds R4 . y = H

A21: for z being Complex st z in N holds

(f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0))

proof

A24:
for x, y being Real st x + (y * <i>) in N & x0 + (y0 * <i>) in N holds
let z be Complex; :: thesis: ( z in N implies (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0)) )

assume A22: z in N ; :: thesis: (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0))

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

end;assume A22: z in N ; :: thesis: (f /. z) - (f /. z0) = ((diff (f,z0)) * (z - z0)) + (R /. (z - z0))

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

(f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>))))

proof

A26:
dom R = COMPLEX
by PARTFUN1:def 2;
let x, y be Real; :: thesis: ( x + (y * <i>) in N & x0 + (y0 * <i>) in N implies (f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>)))) )

assume A25: ( x + (y * <i>) in N & x0 + (y0 * <i>) in N ) ; :: thesis: (f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>))))

then ( f . (x + (y * <i>)) = f /. (x + (y * <i>)) & f . (x0 + (y0 * <i>)) = f /. (x0 + (y0 * <i>)) ) by A17, PARTFUN1:def 6;

hence (f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>)))) by A21, A25, A6; :: thesis: verum

end;assume A25: ( x + (y * <i>) in N & x0 + (y0 * <i>) in N ) ; :: thesis: (f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>))))

then ( f . (x + (y * <i>)) = f /. (x + (y * <i>)) & f . (x0 + (y0 * <i>)) = f /. (x0 + (y0 * <i>)) ) by A17, PARTFUN1:def 6;

hence (f . (x + (y * <i>))) - (f . (x0 + (y0 * <i>))) = ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y * <i>)) - (x0 + (y0 * <i>)))) by A21, A25, A6; :: thesis: verum

for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 )

proof

then reconsider R4 = R4 as RestFunc by FDIFF_1:def 2;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R4 /* h) is convergent & lim ((h ") (#) (R4 /* h)) = 0 )

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 = <i> (#) hz0;

reconsider hz = <i> (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;

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

end;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 = <i> (#) hz0;

reconsider hz = <i> (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;

now :: thesis: for n being Nat holds ((h ") (#) (R4 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)

then A33:
(h ") (#) (R4 /* h) = Re ((hz ") (#) (R /* hz))
by COMSEQ_3:def 5;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: ((h ") (#) (R4 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)

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) * <i> by VALUED_1:6;

reconsider hn = h . n as Real ;

(h . n) * <i> in COMPLEX by XCMPLX_0:def 2;

then A32: (h . n) * <i> 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_{4}(hn)
by A20

.= ((h . n) ") * ((Im R) . ((h . n) * <i>))

.= ((Re ((h . n) ")) * (Im (R . ((h . n) * <i>)))) + ((Re (R . ((h . n) * <i>))) * (Im ((h . n) "))) by A32, A30, COMSEQ_3:def 4

.= Im ((((hz . n) / <i>) ") * (R . (hz . n))) by A31, COMPLEX1:9

.= Im ((<i> / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213

.= Im ((<i> * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10

.= Im (<i> * (((hz ") . n) * (R . (hz . n))))

.= ((Re <i>) * (Im (((hz ") . n) * (R /. (hz . n))))) + ((Re (((hz ") . n) * (R /. (hz . n)))) * (Im <i>)) 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: verum

end;dom R4 = REAL by PARTFUN1:def 2;

then A28: rng h c= dom R4 ;

let n be Nat; :: thesis: ((h ") (#) (R4 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)

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) * <i> by VALUED_1:6;

reconsider hn = h . n as Real ;

(h . n) * <i> in COMPLEX by XCMPLX_0:def 2;

then A32: (h . n) * <i> 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

.= ((h . n) ") * ((Im R) . ((h . n) * <i>))

.= ((Re ((h . n) ")) * (Im (R . ((h . n) * <i>)))) + ((Re (R . ((h . n) * <i>))) * (Im ((h . n) "))) by A32, A30, COMSEQ_3:def 4

.= Im ((((hz . n) / <i>) ") * (R . (hz . n))) by A31, COMPLEX1:9

.= Im ((<i> / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213

.= Im ((<i> * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10

.= Im (<i> * (((hz ") . n) * (R . (hz . n))))

.= ((Re <i>) * (Im (((hz ") . n) * (R /. (hz . n))))) + ((Re (((hz ") . n) * (R /. (hz . n)))) * (Im <i>)) 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: verum

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

deffunc H

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

for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (R2 /* h) is convergent & lim ((h ") (#) (R2 /* h)) = 0 )

proof

then reconsider R2 = R2 as RestFunc by FDIFF_1:def 2;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R2 /* h) is convergent & lim ((h ") (#) (R2 /* h)) = 0 )

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 = <i> (#) hz0;

reconsider hz = <i> (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;

A36: (hz ") (#) (R /* hz) is convergent by CFDIFF_1:def 3;

dom R = COMPLEX by PARTFUN1:def 2;

then A37: rng hz c= dom R ;

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

end;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 = <i> (#) hz0;

reconsider hz = <i> (#) hz0 as non-zero 0 -convergent Complex_Sequence by Lm5;

A36: (hz ") (#) (R /* hz) is convergent by CFDIFF_1:def 3;

dom R = COMPLEX by PARTFUN1:def 2;

then A37: rng hz c= dom R ;

now :: thesis: for n being Nat holds ((h ") (#) (R2 /* h)) . n = - ((Im ((hz ") (#) (R /* hz))) . n)

then A43:
(h ") (#) (R2 /* h) = - (Im ((hz ") (#) (R /* hz)))
by SEQ_1:10;
dom R2 = REAL
by PARTFUN1:def 2;

then A38: rng h c= dom R2 ;

let n be Nat; :: thesis: ((h ") (#) (R2 /* h)) . n = - ((Im ((hz ") (#) (R /* hz))) . n)

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) * <i> by VALUED_1:6;

dom (Re R) = COMPLEX by Th1;

then A41: (h . n) * <i> 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_{5}(hn)
by A35

.= ((h . n) ") * ((Re R) . ((h . n) * <i>))

.= ((Re ((h . n) ")) * (Re (R . ((h . n) * <i>)))) - ((Im ((h . n) ")) * (Im (R . ((h . n) * <i>)))) by A41, A39, COMSEQ_3:def 3

.= Re ((((hz . n) / <i>) ") * (R . (hz . n))) by A40, COMPLEX1:9

.= Re ((<i> / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213

.= Re ((<i> * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10

.= Re (<i> * (((hz ") . n) * (R . (hz . n))))

.= ((Re <i>) * (Re (((hz ") . n) * (R . (hz . n))))) - ((Im <i>) * (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: verum

end;then A38: rng h c= dom R2 ;

let n be Nat; :: thesis: ((h ") (#) (R2 /* h)) . n = - ((Im ((hz ") (#) (R /* hz))) . n)

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) * <i> by VALUED_1:6;

dom (Re R) = COMPLEX by Th1;

then A41: (h . n) * <i> 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

.= ((h . n) ") * ((Re R) . ((h . n) * <i>))

.= ((Re ((h . n) ")) * (Re (R . ((h . n) * <i>)))) - ((Im ((h . n) ")) * (Im (R . ((h . n) * <i>)))) by A41, A39, COMSEQ_3:def 3

.= Re ((((hz . n) / <i>) ") * (R . (hz . n))) by A40, COMPLEX1:9

.= Re ((<i> / (hz . n)) * (R . (hz . n))) by XCMPLX_1:213

.= Re ((<i> * ((hz ") . n)) * (R . (hz . n))) by VALUED_1:10

.= Re (<i> * (((hz ") . n) * (R . (hz . n))))

.= ((Re <i>) * (Re (((hz ") . n) * (R . (hz . n))))) - ((Im <i>) * (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: verum

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

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 * <i>) in N

proof

A48:
for x, y being Real holds (diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>))) = (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * <i>)
let y be Real; :: thesis: ( y in Ny0 implies x0 + (y * <i>) in N )

|.((x0 + (y * <i>)) - z0).| = |.((y - y0) * <i>).| by A6;

then A47: |.((x0 + (y * <i>)) - z0).| = |.(y - y0).| * |.<i>.| by COMPLEX1:65;

assume y in Ny0 ; :: thesis: x0 + (y * <i>) in N

then ( x0 + (y * <i>) is Complex & |.((x0 + (y * <i>)) - z0).| < r0 ) by A47, COMPLEX1:49, RCOMP_1:1;

then x0 + (y * <i>) in { w where w is Complex : |.(w - z0).| < r0 } ;

hence x0 + (y * <i>) in N by A45; :: thesis: verum

end;|.((x0 + (y * <i>)) - z0).| = |.((y - y0) * <i>).| by A6;

then A47: |.((x0 + (y * <i>)) - z0).| = |.(y - y0).| * |.<i>.| by COMPLEX1:65;

assume y in Ny0 ; :: thesis: x0 + (y * <i>) in N

then ( x0 + (y * <i>) is Complex & |.((x0 + (y * <i>)) - z0).| < r0 ) by A47, COMPLEX1:49, RCOMP_1:1;

then x0 + (y * <i>) in { w where w is Complex : |.(w - z0).| < r0 } ;

hence x0 + (y * <i>) in N by A45; :: thesis: verum

proof

A49:
for x, y being Real holds Re ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))
let x, y be Real; :: thesis: (diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>))) = (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))) + ((((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))) * <i>)

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

end;thus (diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>))) = ((Re (diff (f,z0))) + ((Im (diff (f,z0))) * <i>)) * ((x - x0) + ((y - y0) * <i>)) 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))) * <i>) ; :: thesis: verum

proof

A50:
for y being Real st y in Ny0 holds
let x, y be Real; :: thesis: Re ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0))

thus Re ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = 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))) * <i>)) by A48

.= ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0)) by COMPLEX1:12 ; :: thesis: verum

end;thus Re ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = 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))) * <i>)) by A48

.= ((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y - y0)) by COMPLEX1:12 ; :: thesis: verum

(u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>)))

proof

A56:
for y being Real st y in Ny0 holds
let y be Real; :: thesis: ( y in Ny0 implies (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>))) )

(x0 + (y * <i>)) - (x0 + (y0 * <i>)) in dom R by A34, XCMPLX_0:def 2;

then A51: (y - y0) * <i> in dom (Re R) by COMSEQ_3:def 3;

assume y in Ny0 ; :: thesis: (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>)))

then A52: x0 + (y * <i>) in N by A46;

then x0 + (y * <i>) in dom f by A17;

then A53: x0 + (y * <i>) in dom (Re f) by COMSEQ_3:def 3;

A54: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A55: x0 + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;

(u . <*x0,y*>) - (u . <*x0,y0*>) = ((Re f) . (x0 + (y * <i>))) - (u . <*x0,y0*>) by A1, A17, A52

.= ((Re f) . (x0 + (y * <i>))) - ((Re f) . (x0 + (y0 * <i>))) by A1, A17, A54

.= (Re (f . (x0 + (y * <i>)))) - ((Re f) . (x0 + (y0 * <i>))) by A53, COMSEQ_3:def 3

.= (Re (f . (x0 + (y * <i>)))) - (Re (f . (x0 + (y0 * <i>)))) by A55, COMSEQ_3:def 3

.= Re ((f . (x0 + (y * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Re (((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A24, A52, A54

.= (Re ((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Re (diff (f,z0))) * (x0 - x0)) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A49

.= (((Re (diff (f,z0))) * 0) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

.= (- ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

.= (- ((Im (diff (f,z0))) * (y - y0))) + (Re (R . ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

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

end;(x0 + (y * <i>)) - (x0 + (y0 * <i>)) in dom R by A34, XCMPLX_0:def 2;

then A51: (y - y0) * <i> in dom (Re R) by COMSEQ_3:def 3;

assume y in Ny0 ; :: thesis: (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff (f,z0))) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>)))

then A52: x0 + (y * <i>) in N by A46;

then x0 + (y * <i>) in dom f by A17;

then A53: x0 + (y * <i>) in dom (Re f) by COMSEQ_3:def 3;

A54: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A55: x0 + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;

(u . <*x0,y*>) - (u . <*x0,y0*>) = ((Re f) . (x0 + (y * <i>))) - (u . <*x0,y0*>) by A1, A17, A52

.= ((Re f) . (x0 + (y * <i>))) - ((Re f) . (x0 + (y0 * <i>))) by A1, A17, A54

.= (Re (f . (x0 + (y * <i>)))) - ((Re f) . (x0 + (y0 * <i>))) by A53, COMSEQ_3:def 3

.= (Re (f . (x0 + (y * <i>)))) - (Re (f . (x0 + (y0 * <i>)))) by A55, COMSEQ_3:def 3

.= Re ((f . (x0 + (y * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Re (((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A24, A52, A54

.= (Re ((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Re (diff (f,z0))) * (x0 - x0)) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A49

.= (((Re (diff (f,z0))) * 0) - ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

.= (- ((Im (diff (f,z0))) * (y - y0))) + (Re (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

.= (- ((Im (diff (f,z0))) * (y - y0))) + (Re (R . ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

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

((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))

proof

A58:
for x, y being Real holds Im ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))
let y be Real; :: thesis: ( y in Ny0 implies ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0)) )

assume A57: y in Ny0 ; :: thesis: ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))

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) * <i>))) by A50, A57

.= (LD3 . (y - y0)) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>))) by A16

.= (LD3 . (y - y0)) + H_{5}(yy0)

.= (LD3 . (y - y0)) + (R2 . (y - y0)) by A35 ; :: thesis: verum

end;assume A57: y in Ny0 ; :: thesis: ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))

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) * <i>))) by A50, A57

.= (LD3 . (y - y0)) + ((Re R) . ((x0 - x0) + ((y - y0) * <i>))) by A16

.= (LD3 . (y - y0)) + H

.= (LD3 . (y - y0)) + (R2 . (y - y0)) by A35 ; :: thesis: verum

proof

A59:
for y being Real st y in Ny0 holds
let x, y be Real; :: thesis: Im ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0))

thus Im ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = 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))) * <i>)) by A48

.= ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0)) by COMPLEX1:12 ; :: thesis: verum

end;thus Im ((diff (f,z0)) * ((x + (y * <i>)) - (x0 + (y0 * <i>)))) = 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))) * <i>)) by A48

.= ((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y - y0)) by COMPLEX1:12 ; :: thesis: verum

(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>)))

proof

A65:
for y being Real st y in Ny0 holds
let y be Real; :: thesis: ( y in Ny0 implies (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>))) )

(x0 + (y * <i>)) - (x0 + (y0 * <i>)) in dom R by A34, XCMPLX_0:def 2;

then A60: (y - y0) * <i> in dom (Im R) by COMSEQ_3:def 4;

assume y in Ny0 ; :: thesis: (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>)))

then A61: x0 + (y * <i>) in N by A46;

then x0 + (y * <i>) in dom f by A17;

then A62: x0 + (y * <i>) in dom (Im f) by COMSEQ_3:def 4;

A63: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A64: x0 + (y0 * <i>) in dom (Im f) by COMSEQ_3:def 4;

(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Im f) . (x0 + (y * <i>))) - (v . <*x0,y0*>) by A2, A17, A61

.= ((Im f) . (x0 + (y * <i>))) - ((Im f) . (x0 + (y0 * <i>))) by A2, A17, A63

.= (Im (f . (x0 + (y * <i>)))) - ((Im f) . (x0 + (y0 * <i>))) by A62, COMSEQ_3:def 4

.= (Im (f . (x0 + (y * <i>)))) - (Im (f . (x0 + (y0 * <i>)))) by A64, COMSEQ_3:def 4

.= Im ((f . (x0 + (y * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Im (((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A24, A61, A63

.= (Im ((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) + (Im (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A58

.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R . ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

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

end;(x0 + (y * <i>)) - (x0 + (y0 * <i>)) in dom R by A34, XCMPLX_0:def 2;

then A60: (y - y0) * <i> in dom (Im R) by COMSEQ_3:def 4;

assume y in Ny0 ; :: thesis: (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff (f,z0))) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>)))

then A61: x0 + (y * <i>) in N by A46;

then x0 + (y * <i>) in dom f by A17;

then A62: x0 + (y * <i>) in dom (Im f) by COMSEQ_3:def 4;

A63: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A64: x0 + (y0 * <i>) in dom (Im f) by COMSEQ_3:def 4;

(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Im f) . (x0 + (y * <i>))) - (v . <*x0,y0*>) by A2, A17, A61

.= ((Im f) . (x0 + (y * <i>))) - ((Im f) . (x0 + (y0 * <i>))) by A2, A17, A63

.= (Im (f . (x0 + (y * <i>)))) - ((Im f) . (x0 + (y0 * <i>))) by A62, COMSEQ_3:def 4

.= (Im (f . (x0 + (y * <i>)))) - (Im (f . (x0 + (y0 * <i>)))) by A64, COMSEQ_3:def 4

.= Im ((f . (x0 + (y * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Im (((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A24, A61, A63

.= (Im ((diff (f,z0)) * ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) + (Im (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R /. ((x0 + (y * <i>)) - (x0 + (y0 * <i>))))) by A58

.= (((Im (diff (f,z0))) * (x0 - x0)) + ((Re (diff (f,z0))) * (y - y0))) + (Im (R . ((x0 + (y * <i>)) - (x0 + (y0 * <i>)))))

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

((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))

proof

let y be Real; :: thesis: ( y in Ny0 implies ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0)) )

assume A66: y in Ny0 ; :: thesis: ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))

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) * <i>))) by A59, A66

.= (LD1 . (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>))) by A11

.= (LD1 . (y - y0)) + H_{4}(yy0)

.= (LD1 . (y - y0)) + (R4 . (y - y0)) by A20 ; :: thesis: verum

end;assume A66: y in Ny0 ; :: thesis: ((v * (reproj (2,xy0))) . y) - ((v * (reproj (2,xy0))) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))

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) * <i>))) by A59, A66

.= (LD1 . (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i>))) by A11

.= (LD1 . (y - y0)) + H

.= (LD1 . (y - y0)) + (R4 . (y - y0)) by A20 ; :: thesis: verum

now :: thesis: for s being object st s in (reproj (2,xy0)) .: Ny0 holds

s in dom v

then
( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom v )
by FUNCT_2:def 1, TARSKI:def 3;s in dom v

let s be object ; :: thesis: ( s in (reproj (2,xy0)) .: Ny0 implies s in dom v )

assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis: s in dom v

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 * <i>) 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: verum

end;assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis: s in dom v

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 * <i>) 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: verum

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: (v * (reproj (1,xy0))) . x = v . <*x,y0*>

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

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

now :: thesis: for s being object st s in (reproj (2,xy0)) .: Ny0 holds

s in dom u

then
( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom u )
by FUNCT_2:def 1, TARSKI:def 3;s in dom u

let s be object ; :: thesis: ( s in (reproj (2,xy0)) .: Ny0 implies s in dom u )

assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis: s in dom u

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 * <i>) 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: verum

end;assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis: s in dom u

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 * <i>) 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: verum

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

consider R3 being Function of REAL,REAL such that

A81: for y being Element of REAL holds R3 . y = H

A82: for h being non-zero 0 -convergent Real_Sequence holds

( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )

proof

deffunc H
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )

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;

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

end;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: for n being Nat holds ((h ") (#) (R3 /* h)) . n = Im (((hz ") (#) (R /* hz)) . n)

then A88:
(h ") (#) (R3 /* h) = Im ((hz ") (#) (R /* hz))
by COMSEQ_3:def 6;
dom R = COMPLEX
by PARTFUN1:def 2;

then A83: rng hz c= dom R ;

let n be Nat; :: thesis: ((h ") (#) (R3 /* h)) . n = Im (((hz ") (#) (R /* hz)) . n)

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_{6}(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: verum

end;then A83: rng hz c= dom R ;

let n be Nat; :: thesis: ((h ") (#) (R3 /* h)) . n = Im (((hz ") (#) (R /* hz)) . n)

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

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

consider R1 being Function of REAL,REAL such that

A89: for x being Element of REAL holds R1 . x = H

reconsider R3 = R3 as RestFunc by A82, FDIFF_1:def 2;

A90: for x being Real st x in Nx0 holds

x + (y0 * <i>) in N

proof

A91:
for x being Real st x in Nx0 holds
let x be Real; :: thesis: ( x in Nx0 implies x + (y0 * <i>) in N )

assume x in Nx0 ; :: thesis: x + (y0 * <i>) in N

then |.(x - x0).| < r0 by RCOMP_1:1;

then ( x + (y0 * <i>) is Complex & |.((x + (y0 * <i>)) - z0).| < r0 ) by A6;

then x + (y0 * <i>) in { y where y is Complex : |.(y - z0).| < r0 } ;

hence x + (y0 * <i>) in N by A45; :: thesis: verum

end;assume x in Nx0 ; :: thesis: x + (y0 * <i>) in N

then |.(x - x0).| < r0 by RCOMP_1:1;

then ( x + (y0 * <i>) is Complex & |.((x + (y0 * <i>)) - z0).| < r0 ) by A6;

then x + (y0 * <i>) in { y where y is Complex : |.(y - z0).| < r0 } ;

hence x + (y0 * <i>) in N by A45; :: thesis: verum

(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>)))

proof

A97:
for x being Real st x in Nx0 holds
let x be Real; :: thesis: ( x in Nx0 implies (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) )

(x + (y0 * <i>)) - (x0 + (y0 * <i>)) 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: (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>)))

then A93: x + (y0 * <i>) in N by A90;

then x + (y0 * <i>) in dom f by A17;

then A94: x + (y0 * <i>) in dom (Im f) by COMSEQ_3:def 4;

A95: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A96: x0 + (y0 * <i>) in dom (Im f) by COMSEQ_3:def 4;

(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im f) . (x + (y0 * <i>))) - (v . <*x0,y0*>) by A2, A17, A93

.= ((Im f) . (x + (y0 * <i>))) - ((Im f) . (x0 + (y0 * <i>))) by A2, A17, A95

.= (Im (f . (x + (y0 * <i>)))) - ((Im f) . (x0 + (y0 * <i>))) by A94, COMSEQ_3:def 4

.= (Im (f . (x + (y0 * <i>)))) - (Im (f . (x0 + (y0 * <i>)))) by A96, COMSEQ_3:def 4

.= Im ((f . (x + (y0 * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Im (((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A24, A93, A95

.= (Im ((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) + (Im (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A58

.= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R . ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))))

.= ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) by A92, COMSEQ_3:def 4 ;

hence (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) ; :: thesis: verum

end;(x + (y0 * <i>)) - (x0 + (y0 * <i>)) 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: (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>)))

then A93: x + (y0 * <i>) in N by A90;

then x + (y0 * <i>) in dom f by A17;

then A94: x + (y0 * <i>) in dom (Im f) by COMSEQ_3:def 4;

A95: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A96: x0 + (y0 * <i>) in dom (Im f) by COMSEQ_3:def 4;

(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im f) . (x + (y0 * <i>))) - (v . <*x0,y0*>) by A2, A17, A93

.= ((Im f) . (x + (y0 * <i>))) - ((Im f) . (x0 + (y0 * <i>))) by A2, A17, A95

.= (Im (f . (x + (y0 * <i>)))) - ((Im f) . (x0 + (y0 * <i>))) by A94, COMSEQ_3:def 4

.= (Im (f . (x + (y0 * <i>)))) - (Im (f . (x0 + (y0 * <i>)))) by A96, COMSEQ_3:def 4

.= Im ((f . (x + (y0 * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Im (((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A24, A93, A95

.= (Im ((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) + (Im (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A58

.= (((Im (diff (f,z0))) * (x - x0)) + ((Re (diff (f,z0))) * (y0 - y0))) + (Im (R . ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))))

.= ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) by A92, COMSEQ_3:def 4 ;

hence (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff (f,z0))) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) ; :: thesis: verum

((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0))

proof

for h being non-zero 0 -convergent Real_Sequence holds
let x be Real; :: thesis: ( x in Nx0 implies ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0)) )

assume A98: x in Nx0 ; :: thesis: ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0))

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 * <i>))) by A91, A98

.= (LD2 . (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) by A9

.= (LD2 . (x - x0)) + H_{6}(xx0)

.= (LD2 . (x - x0)) + (R3 . xx0) by A81

.= (LD2 . (x - x0)) + (R3 . (x - x0)) ;

:: thesis: verum

end;assume A98: x in Nx0 ; :: thesis: ((v * (reproj (1,xy0))) . x) - ((v * (reproj (1,xy0))) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0))

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 * <i>))) by A91, A98

.= (LD2 . (x - x0)) + ((Im R) . ((x - x0) + (0 * <i>))) by A9

.= (LD2 . (x - x0)) + H

.= (LD2 . (x - x0)) + (R3 . xx0) by A81

.= (LD2 . (x - x0)) + (R3 . (x - x0)) ;

:: thesis: verum

( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )

proof

then reconsider R1 = R1 as RestFunc by FDIFF_1:def 2;
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )

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;

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

end;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: for n being Nat holds ((h ") (#) (R1 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)

then A104:
(h ") (#) (R1 /* h) = Re ((hz ") (#) (R /* hz))
by COMSEQ_3:def 5;
dom R = COMPLEX
by PARTFUN1:def 2;

then A99: rng hz c= dom R ;

let n be Nat; :: thesis: ((h ") (#) (R1 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)

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_{7}(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: verum

end;then A99: rng hz c= dom R ;

let n be Nat; :: thesis: ((h ") (#) (R1 /* h)) . n = Re (((hz ") (#) (R /* hz)) . n)

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

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

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

A107:
for x being Real st x in Nx0 holds
let x be Element of REAL ; :: thesis: (u * (reproj (1,xy0))) . x = u . <*x,y0*>

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

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

(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>)))

proof

A113:
for x being Real st x in Nx0 holds
let x be Real; :: thesis: ( x in Nx0 implies (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) )

(x + (y0 * <i>)) - (x0 + (y0 * <i>)) 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: (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>)))

then A109: x + (y0 * <i>) in N by A90;

then x + (y0 * <i>) in dom f by A17;

then A110: x + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;

A111: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A112: x0 + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;

(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re f) . (x + (y0 * <i>))) - (u . <*x0,y0*>) by A1, A17, A109

.= ((Re f) . (x + (y0 * <i>))) - ((Re f) . (x0 + (y0 * <i>))) by A1, A17, A111

.= (Re (f . (x + (y0 * <i>)))) - ((Re f) . (x0 + (y0 * <i>))) by A110, COMSEQ_3:def 3

.= (Re (f . (x + (y0 * <i>)))) - (Re (f . (x0 + (y0 * <i>)))) by A112, COMSEQ_3:def 3

.= Re ((f . (x + (y0 * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Re (((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A24, A109, A111

.= (Re ((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) + (Re (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A49

.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R . ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))))

.= ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) by A108, COMSEQ_3:def 3 ;

hence (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) ; :: thesis: verum

end;(x + (y0 * <i>)) - (x0 + (y0 * <i>)) 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: (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>)))

then A109: x + (y0 * <i>) in N by A90;

then x + (y0 * <i>) in dom f by A17;

then A110: x + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;

A111: x0 + (y0 * <i>) in N by A6, CFDIFF_1:7;

then x0 + (y0 * <i>) in dom f by A17;

then A112: x0 + (y0 * <i>) in dom (Re f) by COMSEQ_3:def 3;

(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re f) . (x + (y0 * <i>))) - (u . <*x0,y0*>) by A1, A17, A109

.= ((Re f) . (x + (y0 * <i>))) - ((Re f) . (x0 + (y0 * <i>))) by A1, A17, A111

.= (Re (f . (x + (y0 * <i>)))) - ((Re f) . (x0 + (y0 * <i>))) by A110, COMSEQ_3:def 3

.= (Re (f . (x + (y0 * <i>)))) - (Re (f . (x0 + (y0 * <i>)))) by A112, COMSEQ_3:def 3

.= Re ((f . (x + (y0 * <i>))) - (f . (x0 + (y0 * <i>)))) by COMPLEX1:19

.= Re (((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))) + (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A24, A109, A111

.= (Re ((diff (f,z0)) * ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) + (Re (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by COMPLEX1:8

.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R /. ((x + (y0 * <i>)) - (x0 + (y0 * <i>))))) by A49

.= (((Re (diff (f,z0))) * (x - x0)) - ((Im (diff (f,z0))) * (y0 - y0))) + (Re (R . ((x + (y0 * <i>)) - (x0 + (y0 * <i>)))))

.= ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) by A108, COMSEQ_3:def 3 ;

hence (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff (f,z0))) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) ; :: thesis: verum

((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))

proof

let x be Real; :: thesis: ( x in Nx0 implies ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) )

assume A114: x in Nx0 ; :: thesis: ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))

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 * <i>))) by A107, A114

.= (LD1 . (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) by A11

.= (LD1 . (x - x0)) + H_{7}(xx0)

.= (LD1 . (x - x0)) + (R1 . xx0) by A89

.= (LD1 . (x - x0)) + (R1 . (x - x0)) ;

:: thesis: verum

end;assume A114: x in Nx0 ; :: thesis: ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))

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 * <i>))) by A107, A114

.= (LD1 . (x - x0)) + ((Re R) . ((x - x0) + (0 * <i>))) by A11

.= (LD1 . (x - x0)) + H

.= (LD1 . (x - x0)) + (R1 . xx0) by A89

.= (LD1 . (x - x0)) + (R1 . (x - x0)) ;

:: thesis: verum

now :: thesis: for s being object st s in (reproj (1,xy0)) .: Nx0 holds

s in dom v

then
( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom v )
by FUNCT_2:def 1, TARSKI:def 3;s in dom v

let s be object ; :: thesis: ( s in (reproj (1,xy0)) .: Nx0 implies s in dom v )

assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis: s in dom v

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 * <i>) 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: verum

end;assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis: s in dom v

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 * <i>) 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: verum

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: for s being object st s in (reproj (1,xy0)) .: Nx0 holds

s in dom u

then
( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom u )
by FUNCT_2:def 1, TARSKI:def 3;s in dom u

let s be object ; :: thesis: ( s in (reproj (1,xy0)) .: Nx0 implies s in dom u )

assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis: s in dom u

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 * <i>) 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: verum

end;assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis: s in dom u

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 * <i>) 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: verum

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