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 x0, y0 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 = 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 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 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & 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
A2: for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) and
A3: for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) and
A4: ( z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & 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 )
consider N being Neighbourhood of z0 such that
P1: ( N c= dom f & ex L being C_LINEAR ex R being C_REST st
( diff f,z0 = L /. 1r & ( for z being Complex st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) by A4, CFDIFF_1:def 7;
consider L being C_LINEAR, R being C_REST such that
P2: ( 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 P1;
P2R: dom R = COMPLEX by PARTFUN1:def 4;
P3: 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: ( z in N implies (f /. z) - (f /. z0) = ((diff f,z0) * (z - z0)) + (R /. (z - z0)) )
assume AS: z in N ; :: thesis: (f /. z) - (f /. z0) = ((diff f,z0) * (z - z0)) + (R /. (z - z0))
consider a0 being Complex such that
ASS: for w being Complex holds L /. w = a0 * w by CFDIFF_1:def 4;
L /. (1r * (z - z0)) = (a0 * 1r ) * (z - z0) by ASS
.= (L /. 1r ) * (z - z0) by ASS ;
hence (f /. z) - (f /. z0) = ((diff f,z0) * (z - z0)) + (R /. (z - z0)) by AS, P2; :: thesis: verum
end;
P4: for x, y being Real st x + (y * <i> ) in N holds
(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 A4, P3;
P5: 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> )
proof
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:29
.= (((Re (diff f,z0)) * (x - x0)) - ((Im (diff f,z0)) * (y - y0))) + ((((Im (diff f,z0)) * (x - x0)) + ((Re (diff f,z0)) * (y - y0))) * <i> ) ; :: thesis: verum
end;
P5r: 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))
proof
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 P5
.= ((Re (diff f,z0)) * (x - x0)) - ((Im (diff f,z0)) * (y - y0)) by COMPLEX1:28 ; :: thesis: verum
end;
P5i: 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))
proof
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 P5
.= ((Im (diff f,z0)) * (x - x0)) + ((Re (diff f,z0)) * (y - y0)) by COMPLEX1:28 ; :: thesis: verum
end;
consider r0 being Real such that
P991: ( 0 < r0 & { y where y is Complex : |.(y - z0).| < r0 } c= N ) by CFDIFF_1:def 5;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by RCOMP_1:def 7, P991;
P9x0: for x being Real st x in Nx0 holds
x + (y0 * <i> ) in N
proof
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 K1: |.(x - x0).| < r0 by RCOMP_1:8;
K2: x + (y0 * <i> ) is Complex by XCMPLX_0:def 2;
|.((x + (y0 * <i> )) - z0).| < r0 by A4, K1;
then x + (y0 * <i> ) in { y where y is Complex : |.(y - z0).| < r0 } by K2;
hence x + (y0 * <i> ) in N by P991; :: thesis: verum
end;
set Ny0 = ].(y0 - r0),(y0 + r0).[;
reconsider Ny0 = ].(y0 - r0),(y0 + r0).[ as Neighbourhood of y0 by RCOMP_1:def 7, P991;
P9y0: for y being Real st y in Ny0 holds
x0 + (y * <i> ) in N
proof
let y be Real; :: thesis: ( y in Ny0 implies x0 + (y * <i> ) in N )
assume K1: y in Ny0 ; :: thesis: x0 + (y * <i> ) in N
K2: x0 + (y * <i> ) is Complex by XCMPLX_0:def 2;
|.((x0 + (y * <i> )) - z0).| = |.((y - y0) * <i> ).| by A4;
then |.((x0 + (y * <i> )) - z0).| = |.(y - y0).| * |.<i> .| by COMPLEX1:151;
then |.((x0 + (y * <i> )) - z0).| < r0 by K1, RCOMP_1:8, COMPLEX1:135;
then x0 + (y * <i> ) in { w where w is Complex : |.(w - z0).| < r0 } by K2;
hence x0 + (y * <i> ) in N by P991; :: thesis: verum
end;
P10u: 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 * <i> )))
proof
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> ))) )
assume P61: x in Nx0 ; :: thesis: (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i> )))
then P611: x + (y0 * <i> ) in N by P9x0;
then x + (y0 * <i> ) in dom f by P1;
then P63: x + (y0 * <i> ) in dom (Re f) by Def2;
P064: x0 + (y0 * <i> ) in N by A4, CFDIFF_1:7;
then x0 + (y0 * <i> ) in dom f by P1;
then P65: x0 + (y0 * <i> ) in dom (Re f) by Def2;
(x + (y0 * <i> )) - (x0 + (y0 * <i> )) in dom R by P2R, XCMPLX_0:def 2;
then P67: x - x0 in dom (Re R) by Def2;
(u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re f) . (x + (y0 * <i> ))) - (u . <*x0,y0*>) by A2, P611, P1
.= ((Re f) . (x + (y0 * <i> ))) - ((Re f) . (x0 + (y0 * <i> ))) by A2, P064, P1
.= (Re (f /. (x + (y0 * <i> )))) - ((Re f) . (x0 + (y0 * <i> ))) by Def2, P63
.= (Re (f /. (x + (y0 * <i> )))) - (Re (f /. (x0 + (y0 * <i> )))) by Def2, P65
.= Re ((f /. (x + (y0 * <i> ))) - (f /. (x0 + (y0 * <i> )))) by COMPLEX1:48
.= Re (((diff f,z0) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) by P4, P61, P9x0
.= (Re ((diff f,z0) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) + (Re (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) by COMPLEX1:19
.= (((Re (diff f,z0)) * (x - x0)) - ((Im (diff f,z0)) * (y0 - y0))) + (Re (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) by P5r
.= ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i> ))) by Def2, P67 ;
hence (u . <*x,y0*>) - (u . <*x0,y0*>) = ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i> ))) ; :: thesis: verum
end;
P11u: 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) * <i> )))
proof
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> ))) )
assume P61: y in Ny0 ; :: thesis: (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff f,z0)) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i> )))
then P611: x0 + (y * <i> ) in N by P9y0;
then x0 + (y * <i> ) in dom f by P1;
then P63: x0 + (y * <i> ) in dom (Re f) by Def2;
P064: x0 + (y0 * <i> ) in N by A4, CFDIFF_1:7;
then x0 + (y0 * <i> ) in dom f by P1;
then P65: x0 + (y0 * <i> ) in dom (Re f) by Def2;
(x0 + (y * <i> )) - (x0 + (y0 * <i> )) in dom R by P2R, XCMPLX_0:def 2;
then P67: (y - y0) * <i> in dom (Re R) by Def2;
(u . <*x0,y*>) - (u . <*x0,y0*>) = ((Re f) . (x0 + (y * <i> ))) - (u . <*x0,y0*>) by A2, P611, P1
.= ((Re f) . (x0 + (y * <i> ))) - ((Re f) . (x0 + (y0 * <i> ))) by A2, P064, P1
.= (Re (f /. (x0 + (y * <i> )))) - ((Re f) . (x0 + (y0 * <i> ))) by Def2, P63
.= (Re (f /. (x0 + (y * <i> )))) - (Re (f /. (x0 + (y0 * <i> )))) by Def2, P65
.= Re ((f /. (x0 + (y * <i> ))) - (f /. (x0 + (y0 * <i> )))) by COMPLEX1:48
.= Re (((diff f,z0) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) by P4, P61, P9y0
.= (Re ((diff f,z0) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) + (Re (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) by COMPLEX1:19
.= (((Re (diff f,z0)) * (x0 - x0)) - ((Im (diff f,z0)) * (y - y0))) + (Re (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) by P5r
.= (- ((Im (diff f,z0)) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i> ))) by Def2, P67 ;
hence (u . <*x0,y*>) - (u . <*x0,y0*>) = (- ((Im (diff f,z0)) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i> ))) ; :: thesis: verum
end;
P10v: 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 * <i> )))
proof
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> ))) )
assume P61: x in Nx0 ; :: thesis: (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i> )))
then P62: x + (y0 * <i> ) in N by P9x0;
then x + (y0 * <i> ) in dom f by P1;
then P63: x + (y0 * <i> ) in dom (Im f) by Def3;
P064: x0 + (y0 * <i> ) in N by A4, CFDIFF_1:7;
then x0 + (y0 * <i> ) in dom f by P1;
then P65: x0 + (y0 * <i> ) in dom (Im f) by Def3;
(x + (y0 * <i> )) - (x0 + (y0 * <i> )) in dom R by P2R, XCMPLX_0:def 2;
then P67: x - x0 in dom (Im R) by Def3;
(v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im f) . (x + (y0 * <i> ))) - (v . <*x0,y0*>) by A3, P1, P62
.= ((Im f) . (x + (y0 * <i> ))) - ((Im f) . (x0 + (y0 * <i> ))) by A3, P1, P064
.= (Im (f /. (x + (y0 * <i> )))) - ((Im f) . (x0 + (y0 * <i> ))) by Def3, P63
.= (Im (f /. (x + (y0 * <i> )))) - (Im (f /. (x0 + (y0 * <i> )))) by Def3, P65
.= Im ((f /. (x + (y0 * <i> ))) - (f /. (x0 + (y0 * <i> )))) by COMPLEX1:48
.= Im (((diff f,z0) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) by P4, P61, P9x0
.= (Im ((diff f,z0) * ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) + (Im (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) by COMPLEX1:19
.= (((Im (diff f,z0)) * (x - x0)) + ((Re (diff f,z0)) * (y0 - y0))) + (Im (R /. ((x + (y0 * <i> )) - (x0 + (y0 * <i> ))))) by P5i
.= ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i> ))) by Def3, P67 ;
hence (v . <*x,y0*>) - (v . <*x0,y0*>) = ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i> ))) ; :: thesis: verum
end;
P11v: 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) * <i> )))
proof
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> ))) )
assume P61: y in Ny0 ; :: thesis: (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff f,z0)) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i> )))
then P611: x0 + (y * <i> ) in N by P9y0;
then x0 + (y * <i> ) in dom f by P1;
then P63: x0 + (y * <i> ) in dom (Im f) by Def3;
P064: x0 + (y0 * <i> ) in N by A4, CFDIFF_1:7;
then x0 + (y0 * <i> ) in dom f by P1;
then P65: x0 + (y0 * <i> ) in dom (Im f) by Def3;
(x0 + (y * <i> )) - (x0 + (y0 * <i> )) in dom R by P2R, XCMPLX_0:def 2;
then P67: (y - y0) * <i> in dom (Im R) by Def3;
(v . <*x0,y*>) - (v . <*x0,y0*>) = ((Im f) . (x0 + (y * <i> ))) - (v . <*x0,y0*>) by A3, P1, P611
.= ((Im f) . (x0 + (y * <i> ))) - ((Im f) . (x0 + (y0 * <i> ))) by A3, P1, P064
.= (Im (f /. (x0 + (y * <i> )))) - ((Im f) . (x0 + (y0 * <i> ))) by Def3, P63
.= (Im (f /. (x0 + (y * <i> )))) - (Im (f /. (x0 + (y0 * <i> )))) by Def3, P65
.= Im ((f /. (x0 + (y * <i> ))) - (f /. (x0 + (y0 * <i> )))) by COMPLEX1:48
.= Im (((diff f,z0) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> )))) + (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) by P4, P61, P9y0
.= (Im ((diff f,z0) * ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) + (Im (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) by COMPLEX1:19
.= (((Im (diff f,z0)) * (x0 - x0)) + ((Re (diff f,z0)) * (y - y0))) + (Im (R /. ((x0 + (y * <i> )) - (x0 + (y0 * <i> ))))) by P5i
.= ((Re (diff f,z0)) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i> ))) by Def3, P67 ;
hence (v . <*x0,y*>) - (v . <*x0,y0*>) = ((Re (diff f,z0)) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i> ))) ; :: thesis: verum
end;
deffunc H1( Real) -> Element of REAL = (Re R) . $1;
consider R1 being Function of REAL ,REAL such that
P500: for x being Real holds R1 . x = H1(x) from FUNCT_2:sch 4();
 deffunc H2( Real) -> Element of REAL = (Re R) . ($1 * <i> );
consider R2 being Function of REAL ,REAL such that
P501: for y being Real holds R2 . y = H2(y) from FUNCT_2:sch 4();
 deffunc H3( Real) -> Element of REAL = (Im R) . $1;
consider R3 being Function of REAL ,REAL such that
P502: for y being Real holds R3 . y = H3(y) from FUNCT_2:sch 4();
 deffunc H4( Real) -> Element of REAL = (Im R) . ($1 * <i> );
consider R4 being Function of REAL ,REAL such that
P503: for y being Real holds R4 . y = H4(y) from FUNCT_2:sch 4();
 Z2: for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 )
proof
let h be convergent_to_0 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:8;
reconsider hz = hz as convergent_to_0 Complex_Sequence by LM08;
now
let n be Element of NAT ; :: thesis: ((h " ) (#) (R1 /* h)) . n = Re (((hz " ) (#) (R /* hz)) . n)
T7: dom R1 = REAL by PARTFUN1:def 4;
then T1: rng h c= dom R1 ;
dom R1 c= dom (Re R) by LM09, T7, NUMBERS:11;
then T2: h . n in dom (Re R) by TARSKI:def 3, T7;
dom R = COMPLEX by PARTFUN1:def 4;
then T3: rng hz c= dom R ;
T4: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
thus ((h " ) (#) (R1 /* h)) . n = ((h " ) . n) * ((R1 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R1 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R1 /. (h . n)) by T1, FUNCT_2:186
.= ((h . n) " ) * ((Re R) . (h . n)) by P500
.= ((Re ((h . n) " )) * (Re (R /. (h . n)))) - ((Im ((h . n) " )) * (Im (R /. (h . n)))) by T2, Def2, T4
.= Re (((h . n) " ) * (R /. (h . n))) by COMPLEX1:24
.= Re (((hz " ) . n) * (R /. (hz . n))) by VALUED_1:10
.= Re (((hz " ) . n) * ((R /* hz) . n)) by T3, FUNCT_2:186
.= Re (((hz " ) (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis: verum
end;
then Z20: (h " ) (#) (R1 /* h) = Re ((hz " ) (#) (R /* hz)) by COMSEQ_3:def 3;
( (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 Z20, COMPLEX1:12, COMSEQ_3:41; :: thesis: verum
end;
reconsider R1 = R1 as REST by FDIFF_1:def 3, Z2;
for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 )
proof
let h be convergent_to_0 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:8;
reconsider hz0 = hz0 as convergent_to_0 Complex_Sequence by LM08;
set hz = <i> (#) hz0;
reconsider hz = <i> (#) hz0 as convergent_to_0 Complex_Sequence by LM11;
Z201: now
let n be Element of NAT ; :: thesis: ((h " ) (#) (R2 /* h)) . n = - ((Im ((hz " ) (#) (R /* hz))) . n)
dom R2 = REAL by PARTFUN1:def 4;
then T1: rng h c= dom R2 ;
dom (Re R) = COMPLEX by LM09;
then T2: (h . n) * <i> in dom (Re R) by XCMPLX_0:def 2;
dom R = COMPLEX by PARTFUN1:def 4;
then T3: rng hz c= dom R ;
T4: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
T8: hz . n = (h . n) * <i> by VALUED_1:6;
thus ((h " ) (#) (R2 /* h)) . n = ((h " ) . n) * ((R2 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R2 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R2 . (h . n)) by T1, FUNCT_2:185
.= ((h . n) " ) * ((Re R) . ((h . n) * <i> )) by P501
.= ((Re ((h . n) " )) * (Re (R /. ((h . n) * <i> )))) - ((Im ((h . n) " )) * (Im (R /. ((h . n) * <i> )))) by T2, Def2, T4
.= Re ((((hz . n) / <i> ) " ) * (R /. (hz . n))) by COMPLEX1:24, T8
.= Re ((<i> / (hz . n)) * (R /. (hz . n))) by XCMPLX_1:215
.= 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:24
.= - (Im (((hz " ) . n) * ((R /* hz) . n))) by COMPLEX1:17, T3, FUNCT_2:186
.= - (Im (((hz " ) (#) (R /* hz)) . n)) by VALUED_1:5
.= - ((Im ((hz " ) (#) (R /* hz))) . n) by COMSEQ_3:def 4 ; :: thesis: verum
end;
Z20: (h " ) (#) (R2 /* h) = - (Im ((hz " ) (#) (R /* hz))) by Z201, SEQ_1:14;
X22: ( (hz " ) (#) (R /* hz) is convergent & lim ((hz " ) (#) (R /* hz)) = 0 ) by CFDIFF_1:def 3;
then ( Im ((hz " ) (#) (R /* hz)) is convergent & lim (Im ((hz " ) (#) (R /* hz))) = Im 0 ) by COMSEQ_3:41;
then lim ((h " ) (#) (R2 /* h)) = - (Im 0 ) by Z20, SEQ_2:24
.= 0 by COMPLEX1:12 ;
hence ( (h " ) (#) (R2 /* h) is convergent & lim ((h " ) (#) (R2 /* h)) = 0 ) by X22, Z20, SEQ_2:23; :: thesis: verum
end;
then reconsider R2 = R2 as REST by FDIFF_1:def 3;
Z6: for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R3 /* h) is convergent & lim ((h " ) (#) (R3 /* h)) = 0 )
proof
let h be convergent_to_0 Real_Sequence; :: thesis: ( (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:8;
reconsider hz = hz as convergent_to_0 Complex_Sequence by LM08;
now
let n be Element of NAT ; :: thesis: ((h " ) (#) (R3 /* h)) . n = Im (((hz " ) (#) (R /* hz)) . n)
T7: dom R3 = REAL by PARTFUN1:def 4;
then T1: rng h c= dom R3 ;
dom R3 c= dom (Im R) by T7, LM09, NUMBERS:11;
then T2: h . n in dom (Im R) by TARSKI:def 3, T7;
dom R = COMPLEX by PARTFUN1:def 4;
then T3: rng hz c= dom R ;
T4: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
thus ((h " ) (#) (R3 /* h)) . n = ((h " ) . n) * ((R3 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R3 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R3 . (h . n)) by T1, FUNCT_2:185
.= ((h . n) " ) * ((Im R) . (h . n)) by P502
.= ((Re ((h . n) " )) * (Im (R /. (h . n)))) + ((Re (R /. (h . n))) * (Im ((h . n) " ))) by T2, Def3, T4
.= Im (((h . n) " ) * (R /. (h . n))) by COMPLEX1:24
.= Im (((hz " ) . n) * (R /. (hz . n))) by VALUED_1:10
.= Im (((hz " ) . n) * ((R /* hz) . n)) by T3, FUNCT_2:186
.= Im (((hz " ) (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis: verum
end;
then Z20: (h " ) (#) (R3 /* h) = Im ((hz " ) (#) (R /* hz)) by COMSEQ_3:def 4;
( (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 Z20, COMSEQ_3:41, COMPLEX1:12; :: thesis: verum
end;
reconsider R3 = R3 as REST by FDIFF_1:def 3, Z6;
Z8: for h being convergent_to_0 Real_Sequence holds
( (h " ) (#) (R4 /* h) is convergent & lim ((h " ) (#) (R4 /* h)) = 0 )
proof
let h be convergent_to_0 Real_Sequence; :: thesis: ( (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:8;
reconsider hz0 = hz0 as convergent_to_0 Complex_Sequence by LM08;
set hz = <i> (#) hz0;
reconsider hz = <i> (#) hz0 as convergent_to_0 Complex_Sequence by LM11;
now
let n be Element of NAT ; :: thesis: ((h " ) (#) (R4 /* h)) . n = Re (((hz " ) (#) (R /* hz)) . n)
dom R4 = REAL by PARTFUN1:def 4;
then T1: rng h c= dom R4 ;
(h . n) * <i> in COMPLEX by XCMPLX_0:def 2;
then T21: (h . n) * <i> in dom (Im R) by LM09;
dom R = COMPLEX by PARTFUN1:def 4;
then T3: rng hz c= dom R ;
T4: ( Im ((h . n) " ) = 0 & Re ((h . n) " ) = (h . n) " ) by COMPLEX1:def 2, COMPLEX1:def 3;
T6: hz . n = (h . n) * <i> by VALUED_1:6;
thus ((h " ) (#) (R4 /* h)) . n = ((h " ) . n) * ((R4 /* h) . n) by SEQ_1:12
.= ((h . n) " ) * ((R4 /* h) . n) by VALUED_1:10
.= ((h . n) " ) * (R4 . (h . n)) by T1, FUNCT_2:185
.= ((h . n) " ) * ((Im R) . ((h . n) * <i> )) by P503
.= ((Re ((h . n) " )) * (Im (R /. ((h . n) * <i> )))) + ((Re (R /. ((h . n) * <i> ))) * (Im ((h . n) " ))) by Def3, T21, T4
.= Im ((((hz . n) / <i> ) " ) * (R /. (hz . n))) by COMPLEX1:24, T6
.= Im ((<i> / (hz . n)) * (R /. (hz . n))) by XCMPLX_1:215
.= 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:24
.= Re (((hz " ) . n) * ((R /* hz) . n)) by T3, FUNCT_2:186, COMPLEX1:17
.= Re (((hz " ) (#) (R /* hz)) . n) by VALUED_1:5 ; :: thesis: verum
end;
then Z20: (h " ) (#) (R4 /* h) = Re ((hz " ) (#) (R /* hz)) by COMSEQ_3:def 3;
( (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 Z20, COMSEQ_3:41, COMPLEX1:12; :: thesis: verum
end;
reconsider R4 = R4 as REST by FDIFF_1:def 3, Z8;
P141: (proj 1,2) . xy0 = xy0 . 1 by PDIFF_1:def 1
.= x0 by A4, FINSEQ_1:61 ;
P142: (proj 2,2) . xy0 = xy0 . 2 by PDIFF_1:def 1
.= y0 by A4, FINSEQ_1:61 ;
P15u: for x being Real holds (u * (reproj 1,xy0)) . x = u . <*x,y0*>
proof
let x be 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:23
.= u . (Replace xy0,1,x) by PDIFF_1:def 5
.= u . <*x,y0*> by A4, FINSEQ_7:15 ;
:: thesis: verum
end;
P15v: for x being Real holds (v * (reproj 1,xy0)) . x = v . <*x,y0*>
proof
let x be Real; :: thesis: (v * (reproj 1,xy0)) . x = v . <*x,y0*>
x in REAL ;
then P1: x in dom (reproj 1,xy0) by PDIFF_1:def 5;
thus (v * (reproj 1,xy0)) . x = v . ((reproj 1,xy0) . x) by P1, FUNCT_1:23
.= v . (Replace xy0,1,x) by PDIFF_1:def 5
.= v . <*x,y0*> by A4, FINSEQ_7:15 ; :: thesis: verum
end;
P16u: for y being Real holds (u * (reproj 2,xy0)) . y = u . <*x0,y*>
proof
let y be Real; :: thesis: (u * (reproj 2,xy0)) . y = u . <*x0,y*>
y in REAL ;
then P1: y in dom (reproj 2,xy0) by PDIFF_1:def 5;
thus (u * (reproj 2,xy0)) . y = u . ((reproj 2,xy0) . y) by P1, FUNCT_1:23
.= u . (Replace xy0,2,y) by PDIFF_1:def 5
.= u . <*x0,y*> by A4, FINSEQ_7:16 ; :: thesis: verum
end;
P16v: for y being Real holds (v * (reproj 2,xy0)) . y = v . <*x0,y*>
proof
let y be Real; :: thesis: (v * (reproj 2,xy0)) . y = v . <*x0,y*>
y in REAL ;
then P1: y in dom (reproj 2,xy0) by PDIFF_1:def 5;
thus (v * (reproj 2,xy0)) . y = v . ((reproj 2,xy0) . y) by P1, FUNCT_1:23
.= v . (Replace xy0,2,y) by PDIFF_1:def 5
.= v . <*x0,y*> by A4, FINSEQ_7:16 ; :: thesis: verum
end;
deffunc H5( Real) -> Element of REAL = (Re (diff f,z0)) * $1;
consider LD1 being Function of REAL ,REAL such that
P17: for x being Real holds LD1 . x = H5(x) from FUNCT_2:sch 4();
 deffunc H6( Real) -> Element of REAL = (Im (diff f,z0)) * $1;
consider LD2 being Function of REAL ,REAL such that
P18: for x being Real holds LD2 . x = H6(x) from FUNCT_2:sch 4();
 deffunc H7( Real) -> Element of REAL = - ((Im (diff f,z0)) * $1);
consider LD3 being Function of REAL ,REAL such that
P19: for x being Real holds LD3 . x = H7(x) from FUNCT_2:sch 4();
 reconsider LD1 = LD1 as LINEAR by FDIFF_1:def 4, P17;
reconsider LD2 = LD2 as LINEAR by FDIFF_1:def 4, P18;
for x being Real holds LD3 . x = (- (Im (diff f,z0))) * x
proof
let x be Real; :: thesis: LD3 . x = (- (Im (diff f,z0))) * x
thus LD3 . x = - ((Im (diff f,z0)) * x) by P19
.= (- (Im (diff f,z0))) * x ; :: thesis: verum
end;
then reconsider LD3 = LD3 as LINEAR by FDIFF_1:def 4;
P30u: 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: ( x in Nx0 implies ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) )
assume AS30: x in Nx0 ; :: thesis: ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))
thus ((u * (reproj 1,xy0)) . x) - ((u * (reproj 1,xy0)) . x0) = (u . <*x,y0*>) - ((u * (reproj 1,xy0)) . x0) by P15u
.= (u . <*x,y0*>) - (u . <*x0,y0*>) by P15u
.= ((Re (diff f,z0)) * (x - x0)) + ((Re R) . ((x - x0) + (0 * <i> ))) by AS30, P10u
.= (LD1 . (x - x0)) + ((Re R) . ((x - x0) + (0 * <i> ))) by P17
.= (LD1 . (x - x0)) + (R1 . (x - x0)) by P500 ; :: thesis: verum
end;
P31u: 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: ( y in Ny0 implies ((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0)) )
assume AS31: y in Ny0 ; :: thesis: ((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) = (LD3 . (y - y0)) + (R2 . (y - y0))
thus ((u * (reproj 2,xy0)) . y) - ((u * (reproj 2,xy0)) . y0) = (u . <*x0,y*>) - ((u * (reproj 2,xy0)) . y0) by P16u
.= (u . <*x0,y*>) - (u . <*x0,y0*>) by P16u
.= (- ((Im (diff f,z0)) * (y - y0))) + ((Re R) . ((x0 - x0) + ((y - y0) * <i> ))) by AS31, P11u
.= (LD3 . (y - y0)) + ((Re R) . ((x0 - x0) + ((y - y0) * <i> ))) by P19
.= (LD3 . (y - y0)) + (R2 . (y - y0)) by P501 ; :: thesis: verum
end;
P40v: 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: ( x in Nx0 implies ((v * (reproj 1,xy0)) . x) - ((v * (reproj 1,xy0)) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0)) )
assume AS40: x in Nx0 ; :: thesis: ((v * (reproj 1,xy0)) . x) - ((v * (reproj 1,xy0)) . x0) = (LD2 . (x - x0)) + (R3 . (x - x0))
thus ((v * (reproj 1,xy0)) . x) - ((v * (reproj 1,xy0)) . x0) = (v . <*x,y0*>) - ((v * (reproj 1,xy0)) . x0) by P15v
.= (v . <*x,y0*>) - (v . <*x0,y0*>) by P15v
.= ((Im (diff f,z0)) * (x - x0)) + ((Im R) . ((x - x0) + (0 * <i> ))) by AS40, P10v
.= (LD2 . (x - x0)) + ((Im R) . ((x - x0) + (0 * <i> ))) by P18
.= (LD2 . (x - x0)) + (R3 . (x - x0)) by P502 ; :: thesis: verum
end;
P41v: 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: ( y in Ny0 implies ((v * (reproj 2,xy0)) . y) - ((v * (reproj 2,xy0)) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0)) )
assume AS41: y in Ny0 ; :: thesis: ((v * (reproj 2,xy0)) . y) - ((v * (reproj 2,xy0)) . y0) = (LD1 . (y - y0)) + (R4 . (y - y0))
thus ((v * (reproj 2,xy0)) . y) - ((v * (reproj 2,xy0)) . y0) = (v . <*x0,y*>) - ((v * (reproj 2,xy0)) . y0) by P16v
.= (v . <*x0,y*>) - (v . <*x0,y0*>) by P16v
.= ((Re (diff f,z0)) * (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i> ))) by AS41, P11v
.= (LD1 . (y - y0)) + ((Im R) . ((x0 - x0) + ((y - y0) * <i> ))) by P17
.= (LD1 . (y - y0)) + (R4 . (y - y0)) by P503 ; :: thesis: verum
end;
PL1: dom (reproj 1,xy0) = REAL by FUNCT_2:def 1;
now
let s be set ; :: 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
PL2: ( x in Nx0 & s = (reproj 1,xy0) . x ) by FUNCT_2:116;
PL3: s = Replace xy0,1,x by PDIFF_1:def 5, PL2
.= <*x,y0*> by A4, FINSEQ_7:15 ;
x + (y0 * <i> ) in N by P9x0, PL2;
hence s in dom u by A2, P1, PL3; :: thesis: verum
end;
then (reproj 1,xy0) .: Nx0 c= dom u by TARSKI:def 3;
then P61: Nx0 c= dom (u * (reproj 1,xy0)) by PL1, FUNCT_3:3;
then P71: u * (reproj 1,xy0) is_differentiable_in (proj 1,2) . xy0 by FDIFF_1:def 5, P30u, P141;
Q51: LD3 . 1 = - ((Im (diff f,z0)) * 1) by P19
.= - (Im (diff f,z0)) ;
QL1: dom (reproj 2,xy0) = REAL by FUNCT_2:def 1;
now
let s be set ; :: 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
PL2: ( y in Ny0 & s = (reproj 2,xy0) . y ) by FUNCT_2:116;
PL3: s = Replace xy0,2,y by PDIFF_1:def 5, PL2
.= <*x0,y*> by A4, FINSEQ_7:16 ;
x0 + (y * <i> ) in N by P9y0, PL2;
hence s in dom u by A2, P1, PL3; :: thesis: verum
end;
then (reproj 2,xy0) .: Ny0 c= dom u by TARSKI:def 3;
then Q61: Ny0 c= dom (u * (reproj 2,xy0)) by QL1, FUNCT_3:3;
then Q71: u * (reproj 2,xy0) is_differentiable_in (proj 2,2) . xy0 by FDIFF_1:def 5, P31u, P142;
then Q74: partdiff u,xy0,2 = - (Im (diff f,z0)) by FDIFF_1:def 6, Q51, Q61, P31u, P142;
R51: LD2 . 1 = (Im (diff f,z0)) * 1 by P18
.= Im (diff f,z0) ;
PL1: dom (reproj 1,xy0) = REAL by FUNCT_2:def 1;
now
let s be set ; :: 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
PL2: ( x in Nx0 & s = (reproj 1,xy0) . x ) by FUNCT_2:116;
PL3: s = Replace xy0,1,x by PDIFF_1:def 5, PL2
.= <*x,y0*> by A4, FINSEQ_7:15 ;
x + (y0 * <i> ) in N by P9x0, PL2;
hence s in dom v by A3, P1, PL3; :: thesis: verum
end;
then (reproj 1,xy0) .: Nx0 c= dom v by TARSKI:def 3;
then R61: Nx0 c= dom (v * (reproj 1,xy0)) by PL1, FUNCT_3:3;
then R71: v * (reproj 1,xy0) is_differentiable_in (proj 1,2) . xy0 by FDIFF_1:def 5, P40v, P141;
S51: LD1 . 1 = (Re (diff f,z0)) * 1 by P17
.= Re (diff f,z0) ;
QL1: dom (reproj 2,xy0) = REAL by FUNCT_2:def 1;
now
let s be set ; :: 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
PL2: ( y in Ny0 & s = (reproj 2,xy0) . y ) by FUNCT_2:116;
PL3: s = Replace xy0,2,y by PDIFF_1:def 5, PL2
.= <*x0,y*> by A4, FINSEQ_7:16 ;
x0 + (y * <i> ) in N by P9y0, PL2;
hence s in dom v by A3, P1, PL3; :: thesis: verum
end;
then (reproj 2,xy0) .: Ny0 c= dom v by TARSKI:def 3;
then S61: Ny0 c= dom (v * (reproj 2,xy0)) by QL1, FUNCT_3:3;
then v * (reproj 2,xy0) is_differentiable_in (proj 2,2) . xy0 by FDIFF_1:def 5, P41v, P142;
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 P71, Q71, Q74, R71, R51, R61, P40v, P141, P61, P30u, S51, S61, P41v, P142, FDIFF_1:def 6, PDIFF_1:def 11; :: thesis: verum