:: Cauchy-Riemann Differential Equations of Complex Functions
:: by Hiroshi Yamazaki , Yasunari Shidama , Chanapat Pacharapokin and Yatsuka Nakamura
::
:: Received April 7, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PARTFUN1, REAL_1, SEQ_1, COMSEQ_1, SEQ_2,
CARD_1, FUNCT_1, COMPLEX1, RELAT_1, NAT_1, ORDINAL2, ARYTM_3, XXREAL_0,
ARYTM_1, FDIFF_1, VALUED_0, XCMPLX_0, VALUED_1, FINSEQ_1, PDIFF_1,
AFINSQ_1, CARD_3, RCOMP_1, TARSKI, CFDIFF_1, FUNCT_2, XXREAL_1, PRE_TOPC,
REAL_NS1, BINOP_2, NORMSP_1, EUCLID, MCART_1, RVSUM_1, SQUARE_1,
SUPINF_2, STRUCT_0, LOPBAN_1, FUNCT_7;
notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1,
BINOP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, BINOP_2, XREAL_0,
COMPLEX1, REAL_1, VALUED_1, SEQ_1, SEQ_2, RLVECT_1, COMSEQ_1, COMSEQ_2,
COMSEQ_3, PRE_TOPC, STRUCT_0, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_7,
SQUARE_1, EUCLID, NORMSP_0, NORMSP_1, REAL_NS1, LOPBAN_1, NFCONT_1,
FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, RCOMP_1;
constructors REAL_1, SQUARE_1, RSSPACE3, SEQ_2, BINOP_2, FINSEQ_7, NFCONT_1,
RCOMP_1, FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, COMSEQ_2, COMSEQ_3,
RVSUM_1, RELSET_1, BINOP_1, NUMBERS, EXTREAL1, FINSEQ_4;
registrations RELSET_1, STRUCT_0, ORDINAL1, MEMBERED, NUMBERS, XBOOLE_0,
XREAL_0, XXREAL_0, XCMPLX_0, FUNCT_2, REAL_NS1, COMSEQ_3, VALUED_0,
VALUED_1, SEQ_4, FDIFF_1, CFDIFF_1, EUCLID, COMSEQ_2, SQUARE_1, RVSUM_1,
CFUNCT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities LOPBAN_1, EUCLID, COMPLEX1, PDIFF_1, VALUED_1, RVSUM_1, XCMPLX_0;
expansions COMPLEX1, PDIFF_1;
theorems TARSKI, ABSVALUE, XBOOLE_1, XREAL_0, EUCLID, XREAL_1, XXREAL_0,
RCOMP_1, RLVECT_1, SEQ_4, COMPLEX1, SEQ_1, SEQ_2, FINSEQ_1, XCMPLX_1,
VALUED_1, BINOP_2, FINSEQ_2, FINSEQ_7, RVSUM_1, RELAT_1, FUNCT_1,
FUNCT_2, NORMSP_1, LOPBAN_1, PARTFUN1, NFCONT_1, FDIFF_1, NDIFF_1,
REAL_NS1, NUMBERS, FUNCT_3, SQUARE_1, CFUNCT_1, CFDIFF_1, PDIFF_1,
XCMPLX_0, COMSEQ_1, COMSEQ_2, COMSEQ_3, JGRAPH_1, VECTSP_1, NORMSP_0,
CARD_1, ORDINAL1;
schemes FUNCT_2;
begin
reserve n, m for Element of NAT;
reserve z for Complex;
Lm1: for seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real
st seq=cseq & seq is convergent & lim seq = rlim holds lim cseq = rlim
proof
let seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real such
that
A1: seq = cseq & seq is convergent & lim seq = rlim;
reconsider clim = rlim as Element of COMPLEX by XCMPLX_0:def 2;
cseq is convergent & for p be Real st 0<p
ex n being Nat st for m being Nat st n<=m holds
|.cseq.m-clim.|<p by A1,SEQ_2:def 7;
hence thesis by COMSEQ_2:def 6;
end;
Lm2: for seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real st seq=
cseq & cseq is convergent & lim cseq = rlim holds lim seq = rlim
proof
let seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real such that
A1: seq = cseq and
A2: cseq is convergent and
A3: lim cseq = rlim;
reconsider clim = rlim as Complex;
A4: for p being Real st 0 < p
ex n being Nat st for m being Nat st n<=m holds |.seq.m - rlim.| < p
by A1,A2,A3,COMSEQ_2:def 6;
seq is convergent by A1,A2;
hence lim seq = rlim by A4,SEQ_2:def 7;
end;
Lm3: for seq be Real_Sequence, cseq be Complex_Sequence st seq=cseq holds seq
is 0-convergent non-zero iff cseq is 0-convergent non-zero
proof
let seq be Real_Sequence, cseq be Complex_Sequence such that
A1: seq = cseq;
thus seq is 0-convergent non-zero implies cseq is 0-convergent non-zero
proof
assume
A2: seq is 0-convergent non-zero;
then
A3: seq is convergent;
lim seq = 0 by A2;
then
A4: lim cseq = 0 by A1,A3,Lm1;
A5: cseq is non-zero by A1,A2;
cseq is convergent by A1,A3;
hence cseq is 0-convergent non-zero by A5,A4,CFDIFF_1:def 1;
end;
assume
A6: cseq is 0-convergent non-zero;
then lim cseq = 0 by CFDIFF_1:def 1;
then
A7: lim seq = 0 by A1,A6,Lm2;
thus seq is 0-convergent non-zero by A1,A6,A7,FDIFF_1:def 1;
end;
theorem Th1:
for f be PartFunc of COMPLEX,COMPLEX st f is total holds dom (Re
f) = COMPLEX & dom (Im f) = COMPLEX
proof
let f be PartFunc of COMPLEX,COMPLEX;
assume f is total;
then dom f = COMPLEX by PARTFUN1:def 2;
hence thesis by COMSEQ_3:def 3,def 4;
end;
Lm4: for seq, cseq be Complex_Sequence st cseq = <i> (#) seq holds seq is
non-zero iff cseq is non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = <i> (#) seq;
thus seq is non-zero implies cseq is non-zero by A1,COMSEQ_1:38;
A2: <i> (#) seq is non-zero implies seq is non-zero
proof
assume
A3: <i> (#) seq is non-zero;
now
let n;
(<i> (#) seq).n <> 0c by A3,COMSEQ_1:4;
then <i> * seq.n <> 0c by VALUED_1:6;
hence seq.n <> 0c;
end;
hence thesis by COMSEQ_1:4;
end;
assume cseq is non-zero;
hence seq is non-zero by A1,A2;
end;
Lm5: for seq, cseq be Complex_Sequence st cseq = <i> (#) seq holds seq is
0-convergent non-zero iff cseq is 0-convergent non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = <i> (#) seq;
thus seq is 0-convergent non-zero implies cseq is 0-convergent non-zero
proof
assume
A2: seq is 0-convergent non-zero;
then lim seq = 0 by CFDIFF_1:def 1;
then
A3: lim (<i> (#) seq) = <i> * 0 by A2,COMSEQ_2:18
.= 0;
<i> (#) seq is non-zero & <i> (#) seq is convergent by A2,COMSEQ_1:38;
hence cseq is 0-convergent non-zero by A1,A3,CFDIFF_1:def 1;
end;
assume
A4: cseq is 0-convergent non-zero;
then
A5: seq is non-zero by A1,Lm4;
(-<i>) (#) (<i> (#) seq ) is convergent by A1,A4;
then ((-<i>) * <i> ) (#) seq is convergent by CFUNCT_1:22;
then
A6: seq is convergent by CFUNCT_1:26;
lim (<i> (#) seq) = 0 by A1,A4,CFDIFF_1:def 1;
then <i> * lim seq = 0 by A6,COMSEQ_2:18;
hence seq is 0-convergent non-zero by A6,A5,CFDIFF_1:def 1;
end;
:: Cauchy-Riemann
theorem Th2:
for f be PartFunc of COMPLEX, COMPLEX, u,v be PartFunc of REAL 2,
REAL, z0 be Complex, x0, y0 be Real,
xy0 be Element of REAL 2 st (for x, y be
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 be 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)
proof
let f be PartFunc of COMPLEX,COMPLEX, u,v be PartFunc of REAL 2,REAL, z0 be
Complex, x00,y00 be Real ,xy0 be Element of REAL 2 such that
A1: for x,y be 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 be 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;
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 LDF2(Real) = In((Im diff(f,z0))* $1,REAL);
consider LD2 be Function of REAL, REAL such that
A8: for x be Element of REAL holds LD2.x = LDF2(x) from FUNCT_2:sch 4;
A9: for x be Real holds LD2.x = (Im diff(f,z0))* x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD2.x = LDF2(x) by A8;
hence thesis;
end;
reconsider LD2 as LinearFunc by A9,FDIFF_1:def 3;
deffunc LDF1(Real) = In((Re diff(f,z0)) * $1,REAL);
consider LD1 be Function of REAL, REAL such that
A10: for x be Element of REAL holds LD1.x = LDF1(x) from FUNCT_2:sch 4;
A11: for x be Real holds LD1.x = (Re diff(f,z0)) * x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD1.x = LDF1(x) by A10;
hence thesis;
end;
A12: for y be Real holds (v*reproj(2,xy0)).y = v.<*x0,y*>
proof
let y be Real;
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*>;
end;
A13: for y be Real holds (u*reproj(2,xy0)).y=u.<*x0,y*>
proof
let y be Real;
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;
end;
A14: proj(2,2).xy0 = xy0.2 by PDIFF_1:def 1
.= y0 by A7,FINSEQ_1:44;
reconsider LD1 as LinearFunc by A11,FDIFF_1:def 3;
deffunc LDF3(Real) = In(-(Im diff(f,z0)) * $1,REAL);
consider LD3 be Function of REAL,REAL such that
A15: for x be Element of REAL holds LD3.x = LDF3(x) from FUNCT_2:sch 4;
A16: for x be Real holds LD3.x = -(Im diff(f,z0)) * x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD3.x = LDF3(x) by A15;
hence thesis;
end;
for x be Real holds LD3.x = (-(Im diff(f,z0)))* x
proof
let x be Real;
thus LD3.x = -(Im diff(f,z0)) * x by A16
.= (-(Im diff(f,z0)))* x;
end;
then reconsider LD3 as LinearFunc by FDIFF_1:def 3;
reconsider 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 be C_LinearFunc, R be 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 be C_LinearFunc, R be C_RestFunc such that
A19: diff(f,z0) = L/.1r & for z be Complex st
z in N holds f/.z-f/.z0 = L/.(z-z0) +R/.(z-z0) by A18;
deffunc RF4(Real) = In((Im R).($1*<i>),REAL);
consider R4 be Function of REAL, REAL such that
A20: for y be Element of REAL holds R4.y =RF4(y) from FUNCT_2:sch 4;
A21: for z be Complex st z in N holds f/.z-f/.z0 = diff(f,z0)*(z-z0)+R/.(z-z0)
proof
let z be Complex;
assume
A22: z in N;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
consider a0 be Complex such that
A23: for w be 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 thesis by A19,A22;
end;
A24: for x,y be Real st x+y*<i> in N & x0+y0*<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>))
proof
let x,y be Real;
assume
A25: x+y*<i> in N & x0+y0*<i> in N;
then f.(x+y*<i>) = f/.(x+y*<i>) & f.(x0+y0*<i>) = f/.(x0+y0*<i>)
by A17,PARTFUN1:def 6;
hence thesis by A21,A25,A6;
end;
A26: dom R = COMPLEX by PARTFUN1:def 2;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R4/*h) is
convergent & lim ((h")(#)(R4/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz0 =h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 as 0-convergent non-zero Complex_Sequence by Lm3;
set hz=<i>(#)hz0;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm5;
now
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;
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,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)"*RF4(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;
end;
then
A33: (h")(#)(R4/*h) = Re ((hz")(#)(R/*hz)) by COMSEQ_3:def 5;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0 by CFDIFF_1:def 3
;
hence thesis by A33,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider R4 as RestFunc by FDIFF_1:def 2;
deffunc RF2(Real) = In((Re R).($1*<i>),REAL);
A34: dom R = COMPLEX by PARTFUN1:def 2;
consider R2 be Function of REAL,REAL such that
A35: for y be Element of REAL holds R2.y =RF2(y) from FUNCT_2:sch 4;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R2/*h) is
convergent & lim ((h")(#)(R2/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz0 =h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 as 0-convergent non-zero Complex_Sequence by Lm3;
set hz=<i>(#)hz0;
reconsider hz as 0-convergent non-zero 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
dom R2=REAL by PARTFUN1:def 2;
then
A38: rng h c= dom R2;
let n be Nat;
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,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)"*(RF2(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;
end;
then
A43: (h")(#)(R2/*h) = - Im ((hz")(#)(R/*hz)) by SEQ_1:10;
lim ((hz")(#)(R/*hz)) = 0 by CFDIFF_1:def 3;
then lim Im ((hz")(#)(R/*hz)) = Im 0 by A36,COMSEQ_3:41;
then lim ((h")(#)(R2/*h)) = -Im 0 by A43,A36,SEQ_2:10
.= 0 by COMPLEX1:4;
hence thesis by A43,A36,SEQ_2:9;
end;
then reconsider R2 as RestFunc by FDIFF_1:def 2;
consider r0 be 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 as Neighbourhood of y0 by A44,RCOMP_1:def 6;
A46: for y be Real st y in Ny0 holds x0+y*<i> in N
proof
let y be Real;
|. (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;
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;
end;
A48: for x, y be 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;
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>;
end;
A49: for x,y be 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;
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;
end;
A50: for y be 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;
(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;
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 thesis;
end;
A56: for y be 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;
assume
A57: y in Ny0;
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) + RF2(yy0)
.= LD3.(y-y0) + R2.(y-y0) by A35;
end;
A58: for x,y be 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;
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;
end;
A59: for y be 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;
(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;
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 thesis;
end;
A65: for y be 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;
assume
A66: y in Ny0;
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) + RF4(yy0)
.= LD1.(y-y0) + R4.(y-y0) by A20;
end;
now
let s be object;
assume s in (reproj(2,xy0)).:Ny0;
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;
end;
then dom (reproj(2,xy0)) = REAL & (reproj(2,xy0)).:Ny0 c= dom v by
FUNCT_2:def 1,TARSKI:def 3;
then
A70: Ny0 c= dom (v*reproj(2,xy0)) by FUNCT_3:3;
then
A71: v*reproj(2,xy0) is_differentiable_in proj(2,2).xy0 by A14,A65,
FDIFF_1:def 4;
A72: for x be Element of REAL holds (v*reproj(1,xy0)).x=v.<*x,y0*>
proof
let x be Element of REAL;
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;
end;
now
let s be object;
assume s in (reproj(2,xy0)).:Ny0;
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;
end;
then dom (reproj(2,xy0)) = REAL & (reproj(2,xy0)).:Ny0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A76: Ny0 c= dom (u*reproj(2,xy0)) by FUNCT_3:3;
then
A77: u*reproj(2,xy0) is_differentiable_in proj(2,2).xy0 by A14,A56,
FDIFF_1:def 4;
LD3.1 = - (Im diff(f,z0))*1 by A16
.= - (Im diff(f,z0));
then
A78: partdiff(u,xy0,2) = -Im diff(f,z0) by A14,A56,A76,A77,FDIFF_1:def 5;
A79: LD1.1 = (Re diff(f,z0))*1 by A11
.= Re diff(f,z0);
A80: proj(1,2).xy0 = xy0.1 by PDIFF_1:def 1
.= x0 by A7,FINSEQ_1:44;
set Nx0 = ].x0-r0,x0+r0.[;
reconsider Nx0 as Neighbourhood of x0 by A44,RCOMP_1:def 6;
deffunc RF3(Real) = In((Im R).$1,REAL);
consider R3 be Function of REAL, REAL such that
A81: for y be Element of REAL holds R3.y =RF3(y) from FUNCT_2:sch 4;
A82: for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R3/*h) is
convergent & lim ((h")(#)(R3/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz =h as Complex_Sequence by FUNCT_2:6;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm3;
now
dom R = COMPLEX by PARTFUN1:def 2;
then
A83: rng hz c= dom R;
let n be Nat;
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,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)"*(RF3(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;
end;
then
A88: (h")(#)(R3/*h) = Im ((hz")(#)(R/*hz)) by COMSEQ_3:def 6;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0
by CFDIFF_1:def 3;
hence thesis by A88,COMPLEX1:4,COMSEQ_3:41;
end;
deffunc RF1(Real) = In((Re R).$1,REAL);
consider R1 be Function of REAL,REAL such that
A89: for x be Element of REAL holds R1.x = RF1(x) from FUNCT_2:sch 4;
reconsider R3 as RestFunc by A82,FDIFF_1:def 2;
A90: for x be Real st x in Nx0 holds x+y0*<i> in N
proof
let x be Real;
assume x in Nx0;
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;
end;
A91: for x be 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;
(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;
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 thesis;
end;
A97: for x be 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;
assume
A98: x in Nx0;
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) + RF3(xx0)
.= LD2.(x-x0) + R3.(xx0) by A81
.= LD2.(x-x0) + R3.(x-x0);
end;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R1/*h) is
convergent & lim ((h")(#)(R1/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz = h as Complex_Sequence by FUNCT_2:6;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm3;
now
dom R= COMPLEX by PARTFUN1:def 2;
then
A99: rng hz c= dom R;
let n be Nat;
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,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)"* RF1(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;
end;
then
A104: (h")(#)(R1/*h) = Re ((hz")(#)(R/*hz)) by COMSEQ_3:def 5;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0
by CFDIFF_1:def 3;
hence thesis by A104,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider R1 as RestFunc by FDIFF_1:def 2;
A105: LD2.1 = (Im diff(f,z0))*1 by A9
.= Im diff(f,z0);
A106: for x be Element of REAL holds (u*reproj(1,xy0)).x=u.<*x,y0*>
proof
let x be Element of REAL;
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;
end;
A107: for x be 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;
(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;
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 thesis;
end;
A113: for x be 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;
assume
A114: x in Nx0;
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) + RF1(xx0)
.= LD1.(x-x0) + R1.(xx0) by A89
.= LD1.(x-x0) + R1.(x-x0);
end;
now
let s be object;
assume s in (reproj(1,xy0)).:Nx0;
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;
end;
then dom (reproj(1,xy0)) = REAL & (reproj(1,xy0)).:Nx0 c= dom v by
FUNCT_2:def 1,TARSKI:def 3;
then
A118: Nx0 c= dom (v*reproj(1,xy0)) by FUNCT_3:3;
then
A119: v*reproj(1,xy0) is_differentiable_in proj(1,2).xy0 by A80,A97,
FDIFF_1:def 4;
now
let s be object;
assume s in (reproj(1,xy0)).:Nx0;
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;
end;
then dom (reproj(1,xy0)) = REAL & (reproj(1,xy0)).:Nx0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A123: Nx0 c= dom (u*reproj(1,xy0)) by FUNCT_3:3;
then u*reproj(1,xy0) is_differentiable_in proj(1,2).xy0 by A80,A113,
FDIFF_1:def 4;
hence thesis by A80,A14,A113,A97,A65,A123,A77,A78,A105,A118,A119,A79,A70,A71,
FDIFF_1:def 5;
end;
Lm6: for x,y be Real,
vx, vy be Point of REAL-NS 1 st vx=<*x*> & vy=<*y*> holds
vx+vy=<*x+y*> & vx-vy = <*x-y*>
proof
let x, y be Real,vx, vy be Point of REAL-NS 1;
assume
A1: vx=<*x*> & vy=<*y*>;
reconsider vx1= vx, vy1 =vy as Element of REAL 1 by REAL_NS1:def 4;
thus vx+vy = vx1+vy1 by REAL_NS1:2
.= <*x+y*> by A1,RVSUM_1:13;
thus vx-vy = vx1-vy1 by REAL_NS1:5
.= <*x-y*> by A1,RVSUM_1:29;
end;
Lm7: for x, y, z, w be Real, vx, vy be Element of REAL 2 st vx = <*x,y*> & vy
= <*z,w*> holds vx+vy = <*x+z,y+w*> & vx-vy = <*x-z,y-w*>
proof
let x, y, z, w be Real, vx, vy be Element of REAL 2;
reconsider x1=x,y1=y,z1=z,w1=w as Element of REAL by XREAL_0:def 1;
assume
A1: vx = <*x,y*> & vy = <*z,w*>;
hence vx + vy = <* addreal.(x1,z1), addreal.(y1,w1) *> by FINSEQ_2:75
.= <*x1+z1,addreal.(y1,w1) *> by BINOP_2:def 9
.= <*x+z,y+w*> by BINOP_2:def 9;
thus vx - vy = <* diffreal.(x1,z1), diffreal.(y1,w1) *> by A1,FINSEQ_2:75
.= <*x1-z1,diffreal.(y1,w1) *> by BINOP_2:def 10
.= <*x-z,y-w*> by BINOP_2:def 10;
end;
Lm8: for x, y, a be Real,
vx be Element of REAL 2 st vx=<*x,y*> holds a*vx=<*
a*x,a*y *>
proof
let x, y, a be Real, vx be Element of REAL 2;
reconsider x1=x,y1=y as Element of REAL by XREAL_0:def 1;
assume vx = <*x,y*>;
hence a*vx = <* (a multreal).x1, (a multreal).y1 *> by FINSEQ_2:36
.= <*a*x1,(a multreal).y1 *> by RVSUM_1:5
.= <*a*x,a*y*> by RVSUM_1:5;
end;
Lm9: for x,y be Real holds <*x,y*> is Point of REAL-NS 2
proof
let x, y be Real;
reconsider x1=x, y1=y as Element of REAL by XREAL_0:def 1;
<*x1,y1*> in REAL 2 by FINSEQ_2:101;
hence thesis by REAL_NS1:def 4;
end;
Lm10: for x, y, z, w be Real, vx, vy be Point of REAL-NS 2 st vx = <*x,y*> &
vy = <*z,w*> holds vx+vy = <*x+z,y+w*> & vx-vy = <*x-z,y-w*>
proof
let x, y, z, w be Real, vx, vy be Point of REAL-NS 2;
assume
A1: vx = <*x,y*> & vy = <*z,w*>;
reconsider vx1 = vx, vy1 = vy as Element of REAL 2 by REAL_NS1:def 4;
thus vx+vy = vx1+vy1 by REAL_NS1:2
.= <*x+z,y+w*> by A1,Lm7;
thus vx-vy = vx1-vy1 by REAL_NS1:5
.= <*x-z,y-w*> by A1,Lm7;
end;
Lm11: for x,y,a be Real,
vx be Point of REAL-NS 2 st vx=<*x,y*> holds a*vx = <*
a*x,a*y *>
proof
let x, y, a be Real, vx be Point of REAL-NS 2;
assume
A1: vx = <*x,y*>;
reconsider vx1 = vx as Element of REAL 2 by REAL_NS1:def 4;
thus a*vx = a*vx1 by REAL_NS1:3
.= <*a*x, a*y *> by A1,Lm8;
end;
Lm12: for u be PartFunc of REAL 2, REAL, xy be Element of REAL 2 st xy in dom
u holds (<>*u).xy = <*u.xy*>
proof
let u be PartFunc of REAL 2, REAL, xy be Element of REAL 2;
assume xy in dom u;
hence (<>*u).xy = (proj(1,1) qua Function" ).(u.xy) by FUNCT_1:13
.= <*u.xy*> by PDIFF_1:1;
end;
Lm13: for u be PartFunc of REAL 2, REAL, x, y be Real st <*x,y*> in dom u
holds (<>*u)/.(<*x,y*>) =<*u/.(<*x,y*>)*>
proof
set W = proj(1,1)qua Function";
let u be PartFunc of REAL 2, REAL;
let x, y be Real;
assume
A1: <*x,y*> in dom u;
rng u c= dom W by PDIFF_1:2;
then dom <>*u = dom u by RELAT_1:27;
hence (<>*u)/.(<*x,y*>) = (<>*u).(<*x,y*>) by A1,PARTFUN1:def 6
.= (proj(1,1) qua Function" ).(u.(<*x,y*>)) by A1,FUNCT_1:13
.= <*u.(<*x,y*>)*> by PDIFF_1:1
.= <*u/.(<*x,y*>)*> by A1,PARTFUN1:def 6;
end;
Lm14: for x,y be Real,z be Complex,v be Element of REAL-NS 2
st z=x+y*<i> & v=<* x,y *> holds |.z.|= ||.v.||
proof
let x, y be Real,z be Complex,v be Element of REAL-NS 2;
assume that
A1: z=x+y*<i> and
A2: v = <* x,y *>;
A3: Im z = y by A1,COMPLEX1:12;
x in REAL & y in REAL by XREAL_0:def 1;
then reconsider xx = <* x,y *> as Element of REAL 2 by FINSEQ_2:101;
A4: |.xx.| = ||.v.|| & Re z = x by A1,A2,COMPLEX1:12,REAL_NS1:1;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
xx1`2 = y by FINSEQ_1:44;
then
A5: (sqr xx).2 = y^2 by VALUED_1:11;
xx1`1 = x by FINSEQ_1:44;
then len sqr xx = 2 & (sqr xx).1 = x^2 by CARD_1:def 7,VALUED_1:11;
then sqr xx = <*x^2,y^2*> by A5,FINSEQ_1:44;
hence thesis by A4,A3,RVSUM_1:77;
end;
Lm15: for x,y be Real,z be Complex st z=x+y*<i>
holds |.z.| <= |.x.|+|.y.|
proof
let x, y be Real,z be Complex;
assume z = x+y*<i>;
then Re z = x & Im z = y by COMPLEX1:12;
hence thesis by COMPLEX1:78;
end;
Lm16: for x, y be Real holds |.x.| <= |.x+y*<i>.| & |.y.| <= |.x+y*<i>.|
proof
let x, y be Real;
set z = x+y*<i>;
Re z = x & Im z = y by COMPLEX1:12;
hence thesis by COMPLEX1:79;
end;
Lm17: for x,y be Real,v be Element of REAL-NS 2 st v=<* x,y *> holds ||.v.||
<= |.x.|+|.y.|
proof
let x, y be Real,v be Element of REAL-NS 2;
reconsider z = x+y*<i> as Complex;
assume v = <* x,y *>;
then |.z.|= ||.v.|| by Lm14;
hence thesis by Lm15;
end;
theorem Th3:
for seq be Real_Sequence holds seq is convergent & lim seq = 0
iff abs seq is convergent & lim abs seq = 0
proof
let seq be Real_Sequence;
thus seq is convergent & lim seq = 0 implies abs seq is convergent & lim abs
seq = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = 0;
lim abs seq = |.0 .| by A1,A2,SEQ_4:14
.= 0 by ABSVALUE:2;
hence thesis by A1;
end;
thus thesis by SEQ_4:15;
end;
theorem Th4:
for X be RealNormSpace, seq be sequence of X holds seq is
convergent & lim seq = 0.X iff ||. seq .|| is convergent & lim ||. seq .|| = 0
proof
let X be RealNormSpace, seq be sequence of X;
thus seq is convergent & lim seq = 0.X implies ||. seq .|| is convergent &
lim ||. seq .|| = 0
proof
assume
A1: seq is convergent & lim seq = 0.X;
then lim ||. seq .|| = ||.0.X.|| by LOPBAN_1:20;
hence thesis by A1,LOPBAN_1:20,NORMSP_1:1;
end;
assume
A2: ||. seq .|| is convergent & lim ||. seq .|| = 0;
A3: now
let p be Real;
assume 0 < p;
then consider m be Nat such that
A4: for n be Nat st m <= n holds |.||. seq .||.n - 0 .| < p
by A2,SEQ_2:def 7;
take m;
hereby
let n be Nat;
assume m <= n;
then |.||. seq .||.n - 0 .| < p by A4;
then
A5: |. ||. seq.n .|| .| < p by NORMSP_0:def 4;
0 <= ||. seq.n .|| by NORMSP_1:4;
then ||. seq.n .|| < p by A5,ABSVALUE:def 1;
hence ||.seq.n-0.X.|| < p by RLVECT_1:13;
end;
end;
then seq is convergent by NORMSP_1:def 6;
hence thesis by A3,NORMSP_1:def 7;
end;
Lm18: for x be Real, vx be Element of REAL-NS 2 st vx = <* x,0 *> holds ||.vx
.|| = |.x.|
proof
let x be Real, vx be Element of REAL-NS 2;
x in REAL & 0 in REAL by XREAL_0:def 1;
then reconsider xx = <* x,0 *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
assume vx = <* x,0 *>;
then
A1: ||.vx.|| = |.xx.| by REAL_NS1:1;
xx1`2 = 0 by FINSEQ_1:44;
then
A2: (sqr xx).2 = 0^2 by VALUED_1:11;
xx1`1 = x by FINSEQ_1:44;
then len sqr xx = 2 & (sqr xx).1 = x^2 by CARD_1:def 7,VALUED_1:11;
then sqr xx = <*x^2,0^2*> by A2,FINSEQ_1:44;
then sqrt Sum sqr xx = sqrt ( x^2+0^2 ) by RVSUM_1:77
.= sqrt ( x^2+0 * 0) by SQUARE_1:def 1;
hence ||.vx.|| = |.x.| by A1,COMPLEX1:72;
end;
Lm19: for x be Real,vx be Element of REAL-NS 2 st vx = <* 0,x*> holds ||.vx.||
= |.x.|
proof
let x be Real, vx be Element of REAL-NS 2;
x in REAL & 0 in REAL by XREAL_0:def 1;
then reconsider xx = <* 0,x *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
assume vx = <* 0,x *>;
then
A1: ||.vx.|| = |.xx.| by REAL_NS1:1;
xx1`2 = x by FINSEQ_1:44;
then
A2: (sqr xx).2 = x^2 by VALUED_1:11;
xx1`1 = 0 by FINSEQ_1:44;
then len sqr xx = 2 & (sqr xx).1 = 0^2 by CARD_1:def 7,VALUED_1:11;
then sqr xx = <*0^2,x^2*> by A2,FINSEQ_1:44;
then sqrt Sum sqr xx = sqrt ( 0^2+x^2 ) by RVSUM_1:77
.= sqrt ( (0 * 0)+x^2 ) by SQUARE_1:def 1
.= sqrt ( x^2 );
hence ||.vx.|| = |.x.| by A1,COMPLEX1:72;
end;
Lm20: for x be Real,vx be Element of REAL-NS 1 st vx = <* x *> holds ||.vx.||
= |.x.|
proof
let x be Real, vx be Element of REAL-NS 1;
reconsider xx = vx as Element of REAL 1 by REAL_NS1:def 4;
reconsider x2 = x^2 as Element of REAL by XREAL_0:def 1;
assume vx = <* x *>;
then sqrt Sum sqr xx = sqrt Sum <*x2*> by RVSUM_1:55;
then
A1: sqrt Sum sqr xx = sqrt (x^2) by RVSUM_1:73;
||.vx.|| = |.xx.| by REAL_NS1:1;
hence ||.vx.|| = |.x.| by A1,COMPLEX1:72;
end;
Lm21: for v be Element of REAL-NS 1 holds |. proj(1,1).v .| = ||.v.||
proof
let v be Element of REAL-NS 1;
reconsider x=proj(1,1).v as Real;
reconsider w=v as Element of REAL 1 by REAL_NS1:def 4;
len w = 1 & w.1 = x by CARD_1:def 7,PDIFF_1:def 1;
then <* x *> = w by FINSEQ_1:40;
hence thesis by Lm20;
end;
theorem Th5:
for u be PartFunc of REAL 2, REAL, x0, y0 be Real,
xy0 be Element
of REAL 2 st xy0 = <*x0,y0*> & <>*u is_differentiable_in xy0 holds u
is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*
partdiff(u,xy0,1) *> = diff(<>*u,xy0).(<* 1,0 *>) & <* partdiff(u,xy0,2) *> =
diff(<>*u,xy0).(<* 0,1 *>)
proof
reconsider ey0 = <* 0, 1 *> as Point of REAL-NS 2 by Lm9;
reconsider ex0 = <* 1, 0 *> as Point of REAL-NS 2 by Lm9;
let u be PartFunc of REAL 2,REAL, x00, y00 be Real,
xy0 be Element of REAL 2
such that
A1: xy0 = <*x00,y00*> and
A2: <>*u is_differentiable_in xy0;
reconsider x0=x00, y0 = y00 as Element of REAL by XREAL_0:def 1;
A3: xy0 = <*x0,y0*> by A1;
set W = proj(1,1)qua Function";
consider g be PartFunc of REAL-NS 2,REAL-NS 1, gxy0 be Point of REAL-NS 2
such that
A4: <>*u=g and
A5: xy0=gxy0 and
A6: g is_differentiable_in gxy0 by A2;
consider N being Neighbourhood of gxy0 such that
A7: N c= dom g and
A8: ex R be RestFunc of REAL-NS 2,REAL-NS 1 st for xy be Point of REAL-NS 2
st xy in N holds g/.xy-g/.gxy0 = diff(g,gxy0).(xy-gxy0) + R/.(xy-gxy0) by A6,
NDIFF_1:def 7;
consider R be RestFunc of REAL-NS 2,REAL-NS 1 such that
A9: for xy be Point of REAL-NS 2 st xy in N holds g/.xy-g/.gxy0 = diff(
g,gxy0).(xy-gxy0) + R/.(xy-gxy0) by A8;
consider r0 be Real such that
A10: 0 < r0 and
A11: {xy where xy is Point of REAL-NS 2: ||.xy-gxy0.|| < r0} c= N by
NFCONT_1:def 1;
consider f be PartFunc of REAL-NS 2,REAL-NS 1, fxy0 be Point of REAL-NS 2
such that
A12: <>*u=f & xy0=fxy0 and
A13: diff(<>*u,xy0)=diff(f,fxy0) by A2,PDIFF_1:def 8;
rng u c= dom W by PDIFF_1:2;
then
A14: dom <>*u = dom u by RELAT_1:27;
A15: for xy be Element of REAL 2,
L1, R1 be Real, z be Element of REAL 2 st
xy in N & z=xy-xy0 & <*L1*>=diff(<>*u,xy0).z & <*R1*>=R.z holds u.xy-u.xy0 = L1
+R1
proof
let xy be Element of REAL 2, L1, R1 be Real, z be Element of REAL 2;
assume that
A16: xy in N and
A17: z=xy-xy0 and
A18: <*L1*>=diff(<>*u,xy0).z and
A19: <*R1*>=R.z;
reconsider zxy=xy as Point of REAL-NS 2 by REAL_NS1:def 4;
A20: zxy-gxy0 = z by A5,A17,REAL_NS1:5;
R is total by NDIFF_1:def 5;
then dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then R/.(zxy-gxy0) = <*R1*> by A19,A20,PARTFUN1:def 6;
then
A21: diff(g,gxy0).(zxy-gxy0) + R/.(zxy-gxy0) = <*L1+R1*> by A4,A5,A12,A13,A18
,A20,Lm6;
A22: xy0 in N by A5,NFCONT_1:4;
then
A23: g/.gxy0 = g.xy0 by A5,A7,PARTFUN1:def 6
.=(<>*u)/.xy0 by A4,A7,A22,PARTFUN1:def 6;
A24: g/.zxy = g.xy by A7,A16,PARTFUN1:def 6
.=(<>*u)/.xy by A4,A7,A16,PARTFUN1:def 6;
A25: g/.zxy-g/.gxy0 = diff(g,gxy0).(zxy-gxy0) + R/.(zxy-gxy0) by A9,A16;
A26: (<>*u)/.xy0 = (<>*u).xy0 by A4,A7,A22,PARTFUN1:def 6
.= <*u.xy0*> by A4,A7,A14,A22,Lm12;
(<>*u)/.xy = (<>*u).xy by A4,A7,A16,PARTFUN1:def 6
.= <*u.xy*> by A4,A7,A14,A16,Lm12;
then g/.zxy-g/.gxy0 = <*u.xy*> -<*u.xy0*> by A24,A23,A26,REAL_NS1:5
.= <*u.xy*> +<*-u.xy0*> by RVSUM_1:20
.= <* u.xy-u.xy0 *> by RVSUM_1:13;
hence u.xy - u.xy0 = (<*L1+R1*>).1 by A25,A21,FINSEQ_1:def 8
.= L1+R1 by FINSEQ_1:def 8;
end;
set Nx0 = ].x0-r0,x0+r0.[;
reconsider Nx0 as Neighbourhood of x0 by A10,RCOMP_1:def 6;
A27: for x be Real st x in Nx0 holds <*x,y0*> in N
proof
let x be Real;
reconsider xy=<*x,y0*> as Point of REAL-NS 2 by Lm9;
x-x0 in REAL & 0 in REAL by XREAL_0:def 1;
then reconsider xx=<* x-x0,0 *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 =xx as Point of TOP-REAL 2 by EUCLID:22;
assume x in Nx0;
then
A28: |.x-x0.| < r0 by RCOMP_1:1;
xx1`2 = 0 by FINSEQ_1:44;
then
A29: |.xx1`2.| = 0 by ABSVALUE:2;
xy-gxy0 =<*x-x0,y0-y0*> by A3,A5,Lm10
.=<* x-x0,0 *>;
then
A30: ||. xy-gxy0 .|| = |.xx.| by REAL_NS1:1;
|.xx1`1.| = |.x-x0.| & |. xx .| <= |.xx1`1.|+|.xx1`2.| by FINSEQ_1:44
,JGRAPH_1:31;
then ||. xy-gxy0 .|| < r0 by A28,A29,A30,XXREAL_0:2;
then xy in {z where z is Point of REAL-NS 2: ||.z-gxy0.|| < r0};
hence thesis by A11;
end;
now
let s be object;
assume s in (reproj(1,xy0)).:Nx0;
then consider x being Element of REAL such that
A31: x in Nx0 and
A32: s = (reproj(1,xy0)).x by FUNCT_2:65;
A33: <* x,y0 *> in N by A27,A31;
s=Replace(xy0,1,x) by A32,PDIFF_1:def 5
.= <* x, y0 *> by A3,FINSEQ_7:13;
hence s in dom u by A4,A7,A14,A33;
end;
then dom (reproj(1,xy0)) = REAL & (reproj(1,xy0)).:Nx0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A34: Nx0 c= dom (u*reproj(1,xy0)) by FUNCT_3:3;
defpred P1[Element of REAL,Element of REAL] means ex vx be Element of REAL 2
st vx=<*$1,0 *> & <*$2*> = R.vx;
A35: now
let x be Element of REAL;
reconsider vx = <*x,In(0,REAL) *> as Element of REAL 2 by FINSEQ_2:101;
R is total by NDIFF_1:def 5;
then
A36: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
vx is Element of REAL-NS 2 by REAL_NS1:def 4;
then R.vx in the carrier of REAL-NS 1 by A36,PARTFUN1:4;
then R.vx is Element of REAL 1 by REAL_NS1:def 4;
then consider y being Element of REAL such that
A37: <*y*> = R.vx by FINSEQ_2:97;
take y;
thus P1[x,y] by A37;
end;
consider R1 be Function of REAL,REAL such that
A38: for x being Element of REAL holds P1[x, R1.x] from FUNCT_2:sch 3(
A35);
A39: now
let x be Real, vx be Element of REAL 2;
assume
A40: vx=<*x,0 *>;
x in REAL by XREAL_0:def 1;
then
ex vx1 be Element of REAL 2 st vx1=<*x,0 *> & <*R1.x*> = R.vx1 by A38;
hence <*R1.x*> = R.vx by A40;
end;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R1/*h) is
convergent & lim ((h")(#)(R1/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
defpred H1[Nat,Element of REAL-NS 2] means $2 = <* h.$1,0 *>;
A41: now
let n be Element of NAT;
<* h.n,In(0,REAL) *> in REAL 2 by FINSEQ_2:101;
then reconsider y = <* h.n, In(0,REAL) *> as Element of REAL-NS 2 by
REAL_NS1:def 4;
take y;
thus H1[n,y];
end;
consider h1 be sequence of REAL-NS 2 such that
A42: for n being Element of NAT holds H1[n, h1.n] from FUNCT_2:sch 3(A41);
A43: for n being Nat holds H1[n, h1.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A42;
end;
reconsider h1 as sequence of REAL-NS 2;
now
let n be Element of NAT;
A44: h1.n =<*h.n,0 *> by A43;
thus ||.h1.|| .n = ||. h1.n .|| by NORMSP_0:def 4
.= |.h.n.| by A44,Lm18
.= (abs(h)).n by VALUED_1:18;
end;
then
A45: ||.h1.|| = abs h by FUNCT_2:63;
set g = (||.h1.||")(#)(R/*h1);
now
let n be Element of NAT;
reconsider v = h1.n as Element of REAL 2 by REAL_NS1:def 4;
dom R1 = REAL by PARTFUN1:def 2;
then
A46: rng h c= dom R1;
A47: h1.n= <* h.n, 0 *> by A43;
R is total by NDIFF_1:def 5;
then
A48: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then
A49: rng h1 c= dom R;
A50: h1.n =<*h.n,0 *> by A43;
A51: R/.(h1.n) = R.v by A48,PARTFUN1:def 6
.= <* R1.(h.n) *> by A39,A47;
thus ||.g.||.n = ||. g.n .|| by NORMSP_0:def 4
.= ||. (||.h1.||").n *(R/*h1) .n .|| by NDIFF_1:def 2
.= ||. ((||.h1.||).n)" *(R/*h1) .n .|| by VALUED_1:10
.= ||. (||.h1.n.||)" *(R/*h1) .n .|| by NORMSP_0:def 4
.= ||. (|.h.n.|)" *(R/*h1) .n .|| by A50,Lm18
.= ||. (|.h.n.|)" *(R/.(h1.n)) .|| by A49,FUNCT_2:109
.= ||. |.(h.n)" .| *(R/.(h1.n)) .|| by COMPLEX1:66
.= |.|.(h.n)" .|.| *||. (R/.(h1.n)) .|| by NORMSP_1:def 1
.= |.(h.n)".|*|.R1.(h.n).| by A51,Lm20
.= |.(h.n)" * (R1.(h.n)) .| by COMPLEX1:65
.= |.(h.n)" * ((R1/*h).n).| by A46,FUNCT_2:108
.= |.(h".n) * (R1/*h).n.| by VALUED_1:10
.= |.(h"(#)(R1/*h)) .n.| by VALUED_1:5
.= abs (h"(#)(R1/*h)) .n by VALUED_1:18;
end;
then
A52: abs ((h")(#)(R1/*h)) = ||.g.|| by FUNCT_2:63;
now
let n be Nat;
A53: h.n <> 0 by SEQ_1:5;
A54: h1.n = <*h.n,0 *> by A43;
now
assume h1.n = 0.(REAL-NS 2);
then h1.n = 0*2 by REAL_NS1:def 4
.= <* 0,0 *> by EUCLID:54,70;
hence contradiction by A54,A53,FINSEQ_1:77;
end;
hence h1.n <> 0.(REAL-NS 2);
end;
then
A55: h1 is non-zero by NDIFF_1:7;
h is convergent & lim h = 0;
then abs h is convergent & lim abs h = 0 by Th3;
then h1 is convergent & lim h1 = 0.(REAL-NS 2) by A45,Th4;
then h1 is (0.(REAL-NS 2))-convergent non-zero by A55,NDIFF_1:def 4;
then (||.h1.||")(#)(R/*h1) is convergent & lim ((||.h1.||")(#)(R/*h1)) =
0.( REAL-NS 1) by NDIFF_1:def 5;
then ||.g.|| is convergent & lim ||.g.|| = 0 by Th4;
hence (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by A52,Th3;
end;
then reconsider R1 as RestFunc by FDIFF_1:def 2;
ex0 is Element of REAL 2 by REAL_NS1:def 4;
then diff(<>*u,xy0).ex0 is Element of REAL 1 by FUNCT_2:5;
then consider Dux be Element of REAL such that
A56: <*Dux*> = diff(<>*u,xy0).ex0 by FINSEQ_2:97;
deffunc LDF1(Real) = In(Dux* $1,REAL);
consider LD1 be Function of REAL,REAL such that
A57: for x be Element of REAL holds LD1.x = LDF1(x) from FUNCT_2:sch 4;
A58: for x be Real holds LD1.x = Dux* x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD1.x = LDF1(x) by A57;
hence thesis;
end;
set Ny0 = ].y0-r0,y0+r0.[;
reconsider Ny0 as Neighbourhood of y0 by A10,RCOMP_1:def 6;
A59: for y be Real st y in Ny0 holds <*x0,y*> in N
proof
let y be Real;
reconsider xy=<*x0,y*> as Point of REAL-NS 2 by Lm9;
0 in REAL & y-y0 in REAL by XREAL_0:def 1;
then reconsider xx=<* 0,y-y0 *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
assume y in Ny0;
then
A60: |.y-y0.| < r0 by RCOMP_1:1;
xx1`1 = 0 by FINSEQ_1:44;
then
A61: |.xx1`1.| = 0 by ABSVALUE:2;
|. xx .| <= |.xx1`1.|+|.xx1`2.| by JGRAPH_1:31;
then
A62: |.xx.| <= |.y-y0.| by A61,FINSEQ_1:44;
xy-gxy0 =<*x0-x0,y-y0*> by A3,A5,Lm10
.=<* 0,y-y0 *>;
then ||. xy-gxy0 .|| = |.xx.| by REAL_NS1:1;
then ||. xy-gxy0 .|| < r0 by A60,A62,XXREAL_0:2;
then xy in {z where z is Point of REAL-NS 2: ||.z-gxy0.|| < r0};
hence thesis by A11;
end;
now
let s be object;
assume s in (reproj(2,xy0)).:Ny0;
then consider y being Element of REAL such that
A63: y in Ny0 and
A64: s = (reproj(2,xy0)).y by FUNCT_2:65;
A65: <* x0,y *> in N by A59,A63;
s=Replace(xy0,2,y) by A64,PDIFF_1:def 5
.= <* x0, y *> by A3,FINSEQ_7:14;
hence s in dom u by A4,A7,A14,A65;
end;
then dom (reproj(2,xy0)) = REAL & (reproj(2,xy0)).:Ny0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A66: Ny0 c= dom (u*reproj(2,xy0)) by FUNCT_3:3;
defpred P2[Element of REAL,Element of REAL] means ex vy be Element of REAL 2
st vy=<* 0,$1 *> & <*$2*> = R.vy;
A67: now
let x be Element of REAL;
reconsider vx = <*In(0,REAL),x *> as Element of REAL 2 by FINSEQ_2:101;
R is total by NDIFF_1:def 5;
then
A68: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
vx is Element of REAL-NS 2 by REAL_NS1:def 4;
then R.vx in the carrier of REAL-NS 1 by A68,PARTFUN1:4;
then R.vx is Element of REAL 1 by REAL_NS1:def 4;
then consider y being Element of REAL such that
A69: <*y*> = R.vx by FINSEQ_2:97;
take y;
thus P2[x,y] by A69;
end;
consider R3 be Function of REAL,REAL such that
A70: for x being Element of REAL holds P2[x, R3.x] from FUNCT_2:sch 3(
A67);
A71: now
let y be Real, vy be Element of REAL 2;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
assume
A72: vy=<* 0,y *>;
ex vy1 be Element of REAL 2 st vy1=<* 0,y *> & <*R3.yy*> = R.vy1 by A70;
hence <*R3.y*> = R.vy by A72;
end;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R3/*h) is
convergent & lim ((h")(#)(R3/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
defpred H1[Nat,Element of REAL-NS 2] means $2= <* 0,h.$1 *>;
A73: now
let n be Element of NAT;
<* In(0,REAL),h.n *> in REAL 2 by FINSEQ_2:101;
then reconsider y = <* 0,h.n *> as Element of REAL-NS 2 by REAL_NS1:def 4
;
take y;
thus H1[n,y];
end;
consider h1 be sequence of REAL-NS 2 such that
A74: for n being Element of NAT holds H1[n, h1.n] from FUNCT_2:sch 3(A73);
A75: for n being Nat holds H1[n, h1.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A74;
end;
reconsider h1 as sequence of REAL-NS 2;
now
let n be Element of NAT;
A76: h1.n = <* 0,h.n *> by A75;
thus ||.h1.||.n = ||. h1.n .|| by NORMSP_0:def 4
.= |.h.n.| by A76,Lm19
.= (abs(h)).n by VALUED_1:18;
end;
then
A77: ||.h1.|| = abs h by FUNCT_2:63;
set g=(||.h1.||")(#)(R/*h1);
now
let n be Element of NAT;
reconsider v = h1.n as Element of REAL 2 by REAL_NS1:def 4;
dom R3 = REAL by PARTFUN1:def 2;
then
A78: rng h c= dom R3;
A79: h1.n= <* 0, h.n *> by A75;
R is total by NDIFF_1:def 5;
then
A80: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then
A81: rng h1 c= dom R;
A82: h1.n =<* 0,h.n *> by A75;
A83: R/.(h1.n) = R.v by A80,PARTFUN1:def 6
.= <* R3.(h.n) *> by A71,A79;
thus ||.g.||.n = ||. g.n .|| by NORMSP_0:def 4
.= ||. (||.h1.||").n *(R/*h1) .n .|| by NDIFF_1:def 2
.= ||. ((||.h1.||).n)" *(R/*h1) .n .|| by VALUED_1:10
.= ||. (||.h1.n.||)" *(R/*h1) .n .|| by NORMSP_0:def 4
.= ||. (|.h.n.|)" *(R/*h1) .n .|| by A82,Lm19
.= ||. (|.h.n.|)" *(R/.(h1.n)) .|| by A81,FUNCT_2:109
.= ||. |.(h.n)" .| *(R/.(h1.n)) .|| by COMPLEX1:66
.= |.|.(h.n)" .|.| *||. (R/.(h1.n)) .|| by NORMSP_1:def 1
.= |.(h.n)".|*|.R3.(h.n).| by A83,Lm20
.= |.(h.n)" * (R3.(h.n)).| by COMPLEX1:65
.= |.(h.n)" * ((R3/*h).n).| by A78,FUNCT_2:108
.= |.(h".n) * (R3/*h).n.| by VALUED_1:10
.= |.(h"(#)(R3/*h)).n.| by VALUED_1:5
.= abs(h"(#)(R3/*h)).n by VALUED_1:18;
end;
then
A84: abs ((h")(#)(R3/*h)) = ||.g.|| by FUNCT_2:63;
now
let n be Nat;
A85: h.n <> 0 by SEQ_1:5;
A86: h1.n = <* 0,h.n *> by A75;
now
assume h1.n = 0.(REAL-NS 2);
then h1.n = 0*2 by REAL_NS1:def 4
.= <* 0,0 *> by EUCLID:54,70;
hence contradiction by A86,A85,FINSEQ_1:77;
end;
hence h1.n <> 0.(REAL-NS 2);
end;
then
A87: h1 is non-zero by NDIFF_1:7;
h is convergent & lim h = 0;
then abs h is convergent & lim abs h = 0 by Th3;
then h1 is convergent & lim h1 = 0.(REAL-NS 2) by A77,Th4;
then h1 is (0.(REAL-NS 2))-convergent non-zero by A87,NDIFF_1:def 4;
then (||.h1.||")(#)(R/*h1) is convergent & lim ((||.h1.||")(#)(R/*h1)) =
0.( REAL-NS 1) by NDIFF_1:def 5;
then ||.g.|| is convergent & lim ||.g.|| = 0 by Th4;
hence (h")(#)(R3/*h) is convergent & lim ((h")(#)(R3/*h)) = 0 by A84,Th3;
end;
then reconsider R3 as RestFunc by FDIFF_1:def 2;
ey0 is Element of REAL 2 by REAL_NS1:def 4;
then diff(<>*u,xy0).ey0 is Element of REAL 1 by FUNCT_2:5;
then consider Duy be Element of REAL such that
A88: <*Duy*> = diff(<>*u,xy0).ey0 by FINSEQ_2:97;
deffunc LDF3(Real) = In(Duy* $1,REAL);
consider LD3 be Function of REAL, REAL such that
A89: for x be Element of REAL holds LD3.x = LDF3(x) from FUNCT_2:sch 4;
A90: for x be Real holds LD3.x = Duy*x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD3.x = LDF3(x) by A89;
hence thesis;
end;
reconsider LD3 as LinearFunc by A90,FDIFF_1:def 3;
A91: LD3.1 = Duy *1 by A90
.=Duy;
A92: for y be Element of REAL holds (u*reproj(2,xy0)).y=u.<*x0,y*>
proof
let y be Element of REAL;
y in REAL;
then y in dom (reproj(2,xy0)) by PDIFF_1:def 5;
hence (u*reproj(2,xy0)).y = u.((reproj(2,xy0)).y) by FUNCT_1:13
.=u.(Replace(xy0,2,y)) by PDIFF_1:def 5
.=u.<*x0,y*> by A3,FINSEQ_7:14;
end;
A93: for y be Real
st y in Ny0 holds (u*reproj(2,xy0)).y - (u*reproj(2,xy0)
).y0 = LD3.(y-y0) + R3.(y-y0)
proof
ey0 is Element of REAL 2 by REAL_NS1:def 4;
then reconsider D1=diff(<>*u,xy0).ey0 as Element of REAL 1 by FUNCT_2:5;
let y be Real;
assume
A94: y in Ny0;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
reconsider xy =<*x0,yy*> as Element of REAL 2 by FINSEQ_2:101;
A95: LD3.(y-y0)= Duy*(y-y0) by A90;
A96: xy-xy0 = <* x0-x0,y-y0 *> by A3,Lm7
.= <* (y-y0)*0,(y-y0)*1 *>
.= (y-y0)* ey0 by Lm11;
A97: diff(f,fxy0) is LinearOperator of REAL-NS 2,REAL-NS 1 by LOPBAN_1:def 9;
(y-y0)*D1 = (y-y0)*(diff(f,fxy0).ey0) by A13,REAL_NS1:3
.= (diff(<>*u,xy0)).(xy-xy0) by A13,A96,A97,LOPBAN_1:def 5;
then
A98: <*LD3.(y-y0)*> = (diff(<>*u,xy0)).(xy-xy0) by A88,A95,RVSUM_1:47;
<* 0, y-y0 *> = <* x0-x0, y-y0 *> .= xy - xy0 by A3,Lm7;
then
A99: <*R3.(y-y0) *> = R.(xy-xy0) by A71;
thus (u*reproj(2,xy0)).y - (u*reproj(2,xy0)).y0
= u.<*x0,yy*> - (u*reproj(2,xy0)).y0 by A92
.= u.xy - u.xy0 by A3,A92
.= LD3. (y-y0) + R3.(y-y0) by A15,A59,A94,A98,A99;
end;
reconsider LD1 as LinearFunc by A58,FDIFF_1:def 3;
A100: LD1.1 = Dux*1 by A58
.= Dux;
A101: for x be Element of REAL holds (u*reproj(1,xy0)).x=u.<*x,y0*>
proof
let x be Element of REAL;
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 A3,FINSEQ_7:13;
end;
A102: for x be Real
st x in Nx0 holds (u*reproj(1,xy0)).x - (u*reproj(1,xy0)
).x0 = LD1.(x-x0) + R1.(x-x0)
proof
ex0 is Element of REAL 2 by REAL_NS1:def 4;
then reconsider D1=diff(<>*u,xy0).ex0 as Element of REAL 1 by FUNCT_2:5;
let x be Real;
assume
A103: x in Nx0;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
reconsider xy =<*xx,y0*> as Element of REAL 2 by FINSEQ_2:101;
A104: LD1. (x-x0)= Dux*(x-x0) by A58;
A105: xy-xy0 = <* x-x0, y0-y0 *> by A3,Lm7
.= <* (x-x0)*1, (x-x0)*0 *>
.= (x-x0)* ex0 by Lm11;
A106: diff(f,fxy0) is LinearOperator of REAL-NS 2,REAL-NS 1 by LOPBAN_1:def 9;
(x-x0)*D1 = (x-x0)*(diff(f,fxy0).ex0) by A13,REAL_NS1:3
.= (diff(<>*u,xy0)).(xy-xy0) by A13,A105,A106,LOPBAN_1:def 5;
then
A107: <*LD1. (x-x0)*> = (diff(<>*u,xy0)).(xy-xy0) by A56,A104,RVSUM_1:47;
<*x-x0,0 *> = <*x-x0,y0-y0 *> .= xy-xy0 by A3,Lm7;
then
A108: <*R1.(x-x0) *> = R.(xy-xy0) by A39;
thus (u*reproj(1,xy0)).x - (u*reproj(1,xy0)).x0
= u.<*xx,y0*> - (u*reproj(1
,xy0)).x0 by A101
.= u.xy - u.xy0 by A3,A101
.= LD1.(x-x0) + R1.(x-x0) by A15,A27,A103,A107,A108;
end;
A109: proj(2,2).xy0=xy0.2 by PDIFF_1:def 1
.= y0 by A3,FINSEQ_1:44;
then
A110: u*reproj(2,xy0) is_differentiable_in proj(2,2).xy0 by A93,A66,
FDIFF_1:def 4;
A111: proj(1,2).xy0=xy0.1 by PDIFF_1:def 1
.= x0 by A3,FINSEQ_1:44;
then u*reproj(1,xy0) is_differentiable_in proj(1,2).xy0 by A102,A34,
FDIFF_1:def 4;
hence thesis by A111,A109,A56,A88,A102,A93,A100,A34,A91,A66,A110,FDIFF_1:def
5;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem
for f be PartFunc of COMPLEX, COMPLEX, u,v be PartFunc of REAL 2, REAL
, z0 be Complex, x0, y0 be Real, xy0 be Element of REAL 2 st (for x,y be Real
st <*x,y*> in dom v holds x+y*<i> in dom f) & (for x,y be 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 be Real
st x+y*<i> in dom f holds <*x,y*> in dom v & v.<*x,y*> = (Im f).(x+y*<i>)) & z0
= x0+y0*<i> & xy0 = <*x0,y0*> & <>*u is_differentiable_in xy0 & <>*v
is_differentiable_in xy0 & partdiff(u,xy0,1) = partdiff(v,xy0,2) & partdiff(u,
xy0,2) = -partdiff(v,xy0,1) holds f is_differentiable_in z0 & u
is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v
is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re
diff(f,z0) = partdiff(u,xy0,1) & Re diff(f,z0) = partdiff(v,xy0,2) & Im diff(f,
z0) =-partdiff(u,xy0,2) & Im diff(f,z0) = partdiff(v,xy0,1)
proof
let f be PartFunc of COMPLEX, COMPLEX, u, v be PartFunc of REAL 2, REAL, z0
be Complex, x0, y0 be Real, xy0 be Element of REAL 2 such that
A1: for x,y be Real st <*x,y*> in dom v holds x+y*<i> in dom f and
A2: for x,y be 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 be Real st x+y*<i> in dom f holds <*x,y*> in dom v & v.<*x,y
*> = (Im f).(x+y*<i>) and
A4: z0 = x0+y0*<i> and
A5: xy0 = <*x0,y0*> and
A6: <>*u is_differentiable_in xy0 and
A7: <>*v is_differentiable_in xy0 and
A8: partdiff(u,xy0,1) = partdiff(v,xy0,2) and
A9: partdiff(u,xy0,2) = -partdiff(v,xy0,1);
A10: ex hu be PartFunc of REAL-NS 2,REAL-NS 1, huxy0 be Point of REAL-NS 2 st
<>*u=hu & xy0=huxy0 & diff(<>*u,xy0)=diff(hu,huxy0) by A6,PDIFF_1:def 8;
A11: ex hv be PartFunc of REAL-NS 2,REAL-NS 1, hvxy0 be Point of REAL-NS 2 st
<>*v=hv & xy0=hvxy0 & diff(<>*v,xy0) = diff(hv,hvxy0) by A7,PDIFF_1:def 8;
consider gu be PartFunc of REAL-NS 2,REAL-NS 1, guxy0 be Point of REAL-NS 2
such that
A12: <>*u=gu and
A13: xy0=guxy0 and
A14: gu is_differentiable_in guxy0 by A6;
consider Nu being Neighbourhood of guxy0 such that
A15: Nu c= dom gu and
A16: ex Ru be RestFunc of REAL-NS 2,REAL-NS 1 st for xy be Point of REAL-NS
2 st xy in Nu holds gu/.xy-gu/.guxy0 = diff(gu,guxy0).(xy-guxy0) + Ru/.(xy-
guxy0) by A14,NDIFF_1:def 7;
consider r1 be Real such that
A17: 0 < r1 and
A18: {xy where xy is Point of REAL-NS 2: ||.xy-guxy0.|| < r1 } c= Nu by
NFCONT_1:def 1;
consider gv be PartFunc of REAL-NS 2,REAL-NS 1, gvxy0 be Point of REAL-NS 2
such that
A19: <>*v=gv and
A20: xy0=gvxy0 and
A21: gv is_differentiable_in gvxy0 by A7;
consider Ru be RestFunc of REAL-NS 2,REAL-NS 1 such that
A22: for xy be Point of REAL-NS 2 st xy in Nu holds gu/.xy-gu/.guxy0 =
diff(gu,guxy0).(xy-guxy0) + Ru/.(xy-guxy0) by A16;
A23: <* partdiff(u,xy0,1) *> = diff(<>*u,xy0).(<* 1,0 *>) & <* partdiff(u,
xy0,2) *> = diff(<>*u,xy0).(<* 0,1 *>) by A5,A6,Th5;
A24: for x, y be Element of REAL st <*x,y*> in Nu holds u.<*x,y*> - u.<*x0,
y0*> = partdiff(u,xy0,1)*(x-x0) + partdiff(u,xy0,2)*(y-y0) + proj(1,1).(Ru.<*x-
x0,y-y0*>)
proof
Ru is total by NDIFF_1:def 5;
then
A25: dom Ru = the carrier of REAL-NS 2 by PARTFUN1:def 2;
rng u c= dom (proj(1,1)qua Function") by PDIFF_1:2;
then
A26: dom <>*u = dom u by RELAT_1:27;
||.guxy0-guxy0.|| < r1 by A17,NORMSP_1:6;
then
guxy0 in {wxy where wxy is Point of REAL-NS 2: ||.wxy-guxy0.|| < r1 };
then
A27: <*x0,y0 *> in Nu by A5,A13,A18;
then gu/.guxy0 = gu.guxy0 by A5,A13,A15,PARTFUN1:def 6
.= (<>*u)/.<*x0,y0 *> by A5,A12,A13,A15,A27,PARTFUN1:def 6
.= <* u/.<*x0,y0 *> *> by A12,A15,A26,A27,Lm13
.= <* u.<*x0,y0 *> *> by A12,A15,A26,A27,PARTFUN1:def 6;
then
A28: proj(1,1).(gu/.guxy0) = u.<*x0,y0 *> by PDIFF_1:1;
<* In(0,REAL),jj *> in REAL 2 by FINSEQ_2:101;
then reconsider e2 = <* 0,1 *> as Point of REAL-NS 2 by REAL_NS1:def 4;
<* jj,In(0,REAL) *> in REAL 2 by FINSEQ_2:101;
then reconsider e1 = <* 1,0 *> as Point of REAL-NS 2 by REAL_NS1:def 4;
let x, y be Element of REAL;
A29: diff(gu,guxy0) is LinearOperator of REAL-NS 2,REAL-NS 1 by LOPBAN_1:def 9;
<*x,y*> in REAL 2 by FINSEQ_2:101;
then reconsider xy = <*x,y*> as Point of REAL-NS 2 by REAL_NS1:def 4;
A30: (y-y0)*e2 = <*(y-y0)*0,(y-y0)*1 *> by Lm11
.= <* 0,(y-y0) *>;
A31: xy-guxy0 = <*x-x0,y-y0*> by A5,A13,Lm10;
assume
A32: <*x,y*> in Nu;
then gu/.xy = gu.xy by A15,PARTFUN1:def 6
.= (<>*u)/.<*x,y*> by A12,A15,A32,PARTFUN1:def 6
.= <* u/.<*x,y*> *> by A12,A15,A32,A26,Lm13
.= <* u.<*x,y*> *> by A12,A15,A32,A26,PARTFUN1:def 6;
then proj(1,1).(gu/.xy ) = u.<*x,y*> by PDIFF_1:1;
then
A33: u.<*x,y*>-u.<*x0,y0*> = proj(1,1).(gu/.xy-gu/.guxy0 ) by A28,PDIFF_1:4
.= proj(1,1).(diff(gu,guxy0).(xy-guxy0) + Ru/.(xy-guxy0)) by A22,A32
.= proj(1,1).(diff(gu,guxy0).(xy-guxy0)) + proj(1,1).(Ru/.(xy-guxy0))
by PDIFF_1:4;
(x-x0)*e1 = <*(x-x0)*1,(x-x0)*0 *> by Lm11
.= <*(x-x0),0 *>;
then (x-x0)*e1 + (y-y0)*e2 = <*(x-x0)+0, 0+(y-y0) *> by A30,Lm10
.=<*(x-x0), (y-y0)*>;
then xy - guxy0 = (x-x0)*e1 + (y-y0)*e2 by A5,A13,Lm10;
then diff(gu,guxy0).(xy-guxy0) = diff(gu,guxy0).((x-x0)*e1) + diff(gu,
guxy0).((y-y0)*e2) by A29,VECTSP_1:def 20
.= (x-x0)* diff(gu,guxy0).e1 + diff(gu,guxy0).((y-y0)*e2) by A29,
LOPBAN_1:def 5
.= (x-x0)* diff(gu,guxy0).e1 + (y-y0)*diff(gu,guxy0).e2 by A29,
LOPBAN_1:def 5;
hence
u.<*x,y*>-u.<*x0,y0*> = proj(1,1).((x-x0)*(diff(gu,guxy0).e1)) + proj
(1,1).((y-y0)*(diff(gu,guxy0).e2)) + proj(1,1).(Ru/.(xy-guxy0)) by A33,
PDIFF_1:4
.= (x-x0)*proj(1,1).((diff(gu,guxy0).e1)) + proj(1,1).((y-y0)*(diff(gu
,guxy0).e2)) + proj(1,1).(Ru/.(xy-guxy0)) by PDIFF_1:4
.= (x-x0)*proj(1,1).(<* partdiff(u,xy0,1) *>) + (y-y0)*proj(1,1).(<*
partdiff(u,xy0,2) *>) + proj(1,1).(Ru/.(xy-guxy0)) by A23,A12,A13,A10,PDIFF_1:4
.= (x-x0)* partdiff(u,xy0,1) + (y-y0)*proj(1,1).(<* partdiff(u,xy0,2)
*>) + proj(1,1).(Ru/.(xy-guxy0)) by PDIFF_1:1
.= (x-x0)*partdiff(u,xy0,1) + (y-y0)*partdiff(u,xy0,2) + proj(1,1).(Ru
/.(xy-guxy0)) by PDIFF_1:1
.= partdiff(u,xy0,1)*(x-x0)+partdiff(u,xy0,2)*(y-y0) + proj(1,1).(Ru.
<*x-x0,y-y0*>) by A31,A25,PARTFUN1:def 6;
end;
consider Nv being Neighbourhood of gvxy0 such that
A34: Nv c= dom gv and
A35: ex Rv be RestFunc of REAL-NS 2,REAL-NS 1 st for xy be Point of REAL-NS
2 st xy in Nv holds gv/.xy-gv/.gvxy0 = diff(gv,gvxy0).(xy-gvxy0) + Rv/.(xy-
gvxy0) by A21,NDIFF_1:def 7;
consider r2 be Real such that
A36: 0 < r2 and
A37: {xy where xy is Point of REAL-NS 2: ||.xy-gvxy0.|| < r2 } c= Nv by
NFCONT_1:def 1;
set r0 = min(r1/2,r2/2);
set N = {y where y is Complex : |.y-z0.| < r0};
consider Rv be RestFunc of REAL-NS 2,REAL-NS 1 such that
A38: for xy be Point of REAL-NS 2 st xy in Nv holds gv/.xy-gv/.gvxy0 =
diff(gv,gvxy0).(xy-gvxy0) + Rv/.(xy-gvxy0) by A35;
A39: <* partdiff(v,xy0,1) *> = diff(<>*v,xy0).(<* 1,0 *>) & <* partdiff(v,
xy0,2) *> = diff(<>*v,xy0).(<* 0,1 *>) by A5,A7,Th5;
A40: for x, y be Element of REAL st <*x,y*> in Nv holds v.<*x,y*>-v.<*x0,y0
*> = partdiff(v,xy0,1)*(x-x0) + partdiff(v,xy0,2)*(y-y0) + proj(1,1).(Rv.<*x-x0
,y-y0*>)
proof
Rv is total by NDIFF_1:def 5;
then
A41: dom Rv = the carrier of REAL-NS 2 by PARTFUN1:def 2;
rng v c= dom (proj(1,1)qua Function") by PDIFF_1:2;
then
A42: dom <>*v = dom v by RELAT_1:27;
||.gvxy0-gvxy0.|| < r2 by A36,NORMSP_1:6;
then gvxy0 in {wxy where wxy is Point of REAL-NS 2 : ||.wxy-gvxy0.|| < r2
};
then
A43: <*x0,y0 *> in Nv by A5,A20,A37;
then gv/.gvxy0 = gv.gvxy0 by A5,A20,A34,PARTFUN1:def 6
.= (<>*v)/.<*x0,y0 *> by A5,A19,A20,A34,A43,PARTFUN1:def 6
.= <* v/.<*x0,y0 *> *> by A19,A34,A42,A43,Lm13
.= <* v.<*x0,y0 *> *> by A19,A34,A42,A43,PARTFUN1:def 6;
then
A44: proj(1,1).(gv/.gvxy0) = v.<*x0,y0 *> by PDIFF_1:1;
<* In(0,REAL),jj *> in REAL 2 by FINSEQ_2:101;
then reconsider e2 = <* 0,1 *> as Point of REAL-NS 2 by REAL_NS1:def 4;
<* jj,In(0,REAL) *> in REAL 2 by FINSEQ_2:101;
then reconsider e1 = <* 1,0 *> as Point of REAL-NS 2 by REAL_NS1:def 4;
let x, y be Element of REAL;
A45: diff(gv,gvxy0) is LinearOperator of REAL-NS 2,REAL-NS 1 by LOPBAN_1:def 9;
<*x,y*> in REAL 2 by FINSEQ_2:101;
then reconsider xy = <*x,y*> as Point of REAL-NS 2 by REAL_NS1:def 4;
A46: (y-y0)*e2 = <*(y-y0)*0,(y-y0)*1 *> by Lm11
.= <* 0,(y-y0) *>;
A47: xy-gvxy0 = <*x-x0,y-y0*> by A5,A20,Lm10;
assume
A48: <*x,y*> in Nv;
then gv/.xy = gv.xy by A34,PARTFUN1:def 6
.=(<>*v)/.<*x,y*> by A19,A34,A48,PARTFUN1:def 6
.=<* v/.<*x,y*> *> by A19,A34,A48,A42,Lm13
.=<* v.<*x,y*> *> by A19,A34,A48,A42,PARTFUN1:def 6;
then proj(1,1).(gv/.xy ) = v.<*x,y*> by PDIFF_1:1;
then
A49: v.<*x,y*>-v.<*x0,y0*> = proj(1,1).(gv/.xy-gv/.gvxy0 ) by A44,PDIFF_1:4
.= proj(1,1).(diff(gv,gvxy0).(xy-gvxy0) + Rv/.(xy-gvxy0)) by A38,A48
.= proj(1,1).(diff(gv,gvxy0).(xy-gvxy0)) + proj(1,1).(Rv/.(xy-gvxy0))
by PDIFF_1:4;
(x-x0)*e1 = <*(x-x0)*1,(x-x0)*0 *> by Lm11
.= <*(x-x0),0 *>;
then (x-x0)*e1 + (y-y0)*e2 = <* (x-x0)+0, 0+(y-y0) *> by A46,Lm10
.= <*(x-x0), (y-y0)*>;
then diff(gv,gvxy0).(xy-gvxy0) = diff(gv,gvxy0).((x-x0)*e1) + diff(gv,
gvxy0).((y-y0)*e2) by A47,A45,VECTSP_1:def 20
.= (x-x0)* diff(gv,gvxy0).e1 + diff(gv,gvxy0).((y-y0)*e2) by A45,
LOPBAN_1:def 5
.= (x-x0)* diff(gv,gvxy0).e1 + (y-y0)*diff(gv,gvxy0).e2 by A45,
LOPBAN_1:def 5;
hence v.<*x,y*>-v.<*x0,y0*> = proj(1,1).((x-x0)* (diff(gv,gvxy0).e1)) +
proj(1,1).((y-y0)* (diff(gv,gvxy0).e2)) + proj(1,1).(Rv/.(xy-gvxy0)) by A49,
PDIFF_1:4
.= (x-x0)*proj(1,1).((diff(gv,gvxy0).e1)) + proj(1,1).((y-y0)* (diff(
gv,gvxy0).e2)) + proj(1,1).(Rv/.(xy-gvxy0)) by PDIFF_1:4
.= (x-x0)*proj(1,1).((diff(gv,gvxy0).e1)) + (y-y0)*proj(1,1).((diff(gv
,gvxy0).e2)) + proj(1,1).(Rv/.(xy-gvxy0)) by PDIFF_1:4
.= (x-x0)* partdiff(v,xy0,1) + (y-y0)*proj(1,1). (<* partdiff(v,xy0,2)
*> ) + proj(1,1).(Rv/.(xy-gvxy0)) by A39,A19,A20,A11,PDIFF_1:1
.= (x-x0)* partdiff(v,xy0,1) + (y-y0)* partdiff(v,xy0,2) + proj(1,1).(
Rv/.(xy-gvxy0)) by PDIFF_1:1
.= partdiff(v,xy0,1)*(x-x0) + partdiff(v,xy0,2)*(y-y0) + proj(1,1).(Rv
.<*x-x0,y-y0*>) by A47,A41,PARTFUN1:def 6;
end;
A50: now
let x, y be Element of REAL;
assume x+y*<i> in N;
then
A51: ex w be Complex st w=x+y*<i> & |.w-z0.| < r0;
<*x,y*> in REAL 2 by FINSEQ_2:101;
then reconsider xy=<*x,y*> as Point of REAL-NS 2 by REAL_NS1:def 4;
rng v c= dom (proj(1,1) qua Function") by PDIFF_1:2;
then
A52: dom <>*v = dom v by RELAT_1:27;
||.gvxy0-gvxy0.|| < r2 by A36,NORMSP_1:6;
then gvxy0 in {wxy where wxy is Point of REAL-NS 2 : ||.wxy-gvxy0.|| < r2
};
then <* x0, y0 *> in Nv by A5,A20,A37;
then
A53: x0+y0*<i> in dom f by A1,A19,A34,A52;
then
A54: x0+y0*<i> in dom (Re f) by COMSEQ_3:def 3;
A55: x0+y0*<i> in dom (Im f) by A53,COMSEQ_3:def 4;
A56: f.(x0+y0*<i>) = Re (f.(x0+y0*<i>)) + Im(f.(x0+y0*<i>))*<i> by COMPLEX1:13
.= (Re f).(x0+y0*<i>) + Im(f.(x0+y0*<i>))*<i> by A54,COMSEQ_3:def 3
.= (Re f).(x0+y0*<i>) + (Im f).(x0+y0*<i>)*<i> by A55,COMSEQ_3:def 4;
|.y-y0.|<=|. (x-x0) + (y-y0)*<i> .| by Lm16;
then
A57: |.y-y0.| < r0 by A4,A51,XXREAL_0:2;
A58: r0 <= r1/2 by XXREAL_0:17;
then
A59: |.y-y0.| < r1/2 by A57,XXREAL_0:2;
|.x-x0.|<=|. (x-x0) + (y-y0)*<i> .| by Lm16;
then
A60: |.x-x0.| < r0 by A4,A51,XXREAL_0:2;
then |.x-x0.| < r1/2 by A58,XXREAL_0:2;
then
A61: |.x-x0.| + |.y-y0.| < r1/2+r1/2 by A59,XREAL_1:8;
xy-guxy0 = <* x-x0,y-y0 *> by A5,A13,Lm10;
then ||.xy-guxy0.|| <=|.x-x0.| + |.y-y0.| by Lm17;
then ||.xy-guxy0.|| < r1 by A61,XXREAL_0:2;
then xy in {wxy where wxy is Point of REAL-NS 2 : ||.wxy-guxy0.|| < r1 };
then
A62: u.<*x,y*> - u.<*x0,y0*> = partdiff(u,xy0,1)*(x-x0)+partdiff(u,xy0,2)
*(y-y0) + proj(1,1).(Ru.<*x-x0,y-y0*>) by A18,A24
.= partdiff(u,xy0,1)*(x-x0)+<i>*partdiff(v,xy0,1)*(y-y0)*<i> + proj(1,
1).(Ru.<*x-x0,y-y0*>) by A9;
A63: r0 <= r2/2 by XXREAL_0:17;
then
A64: |.y-y0.| < r2/2 by A57,XXREAL_0:2;
|.x-x0.| < r2/2 by A63,A60,XXREAL_0:2;
then
A65: |.x-x0.| + |.y-y0.| < r2/2+r2/2 by A64,XREAL_1:8;
xy-gvxy0 = <* x-x0,y-y0 *> by A5,A20,Lm10;
then ||.xy-gvxy0.|| <=|.x-x0.| + |.y-y0.| by Lm17;
then ||.xy-gvxy0.|| < r2 by A65,XXREAL_0:2;
then
A66: xy in {wxy where wxy is Point of REAL-NS 2 : ||.wxy-gvxy0.|| < r2 };
then
A67: (v.<*x,y*>-v.<*x0,y0*>)*<i> = (partdiff(v,xy0,1)*(x-x0)+partdiff(u,
xy0,1)*(y-y0) + proj(1,1).(Rv.<*x-x0,y-y0*>))*<i> by A8,A37,A40;
<*x,y *> in Nv by A37,A66;
then
A68: x+y*<i> in dom f by A1,A19,A34,A52;
then
A69: x+y*<i> in dom (Re f) by COMSEQ_3:def 3;
A70: f/.(x+y*<i>) = f.(x+y*<i>) & f/.(x0+y0*<i>) = f.(x0+y0*<i>)
by A53,A68,PARTFUN1:def 6;
A71: x+y*<i> in dom (Im f ) by A68,COMSEQ_3:def 4;
f.(x+y*<i>) = Re (f.(x+y*<i>)) + Im(f.(x+y*<i>))*<i> by COMPLEX1:13
.= (Re f).(x+y*<i>) + Im(f.(x+y*<i>))*<i> by A69,COMSEQ_3:def 3
.=(Re f).(x+y*<i>) + (Im f).(x+y*<i>)*<i> by A71,COMSEQ_3:def 4;
then f.(x+y*<i>) - f.(x0+y0*<i>) = (u.<*x,y*> + ((Im f).(x+y*<i>))*<i>)
-((Re f).(x0+y0*<i>) + ((Im f).(x0+y0*<i>))*<i>) by A2,A68,A56
.=(u.<*x,y*> + ( v.<*x,y*> ) * <i> ) -((Re f).(x0+y0*<i>) + ((Im f).(
x0+y0*<i>)) * <i> ) by A3,A68
.=(u.<*x,y*> + ( v.<*x,y*> )*<i>) -(u.<*x0,y0 *> + ((Im f).(x0+y0*<i>)
) * <i> ) by A2,A53
.= (u.<*x,y*> + ( v.<*x,y*> ) * <i> ) -(u.<*x0,y0 *> + ( v.<*x0,y0*> )
* <i> ) by A3,A53
.= (u.<*x,y*> - u.<*x0,y0*>) + (v.<*x,y*>- v.<*x0,y0*>) *<i>;
hence
f/.(x+y*<i>) - f/.(x0+y0*<i>) =(partdiff(u,xy0,1)+<i>*partdiff(v,xy0,
1)) *((x-x0)+(y-y0)*<i>) + (proj(1,1).(Ru.<*x-x0,y-y0*>) + (proj(1,1).(Rv.<*x-
x0,y-y0*>))*<i>) by A70,A62,A67;
end;
A72: for x,y be Element of REAL st x+y*<i> in N holds |.x-x0.|<r1/2 & |.y
-y0.|<r1/2 & |.x-x0.|<r2/2 & |.y-y0.|<r2/2
proof
let x, y be Element of REAL;
assume x+y*<i> in N;
then
A73: ex w be Complex st w=x+y*<i> & |.w-z0.| < r0;
|.x-x0.| <= |. (x-x0) + (y-y0)*<i> .| by Lm16;
then
A74: |.x-x0.| < r0 by A4,A73,XXREAL_0:2;
A75: r0 <=r1/2 by XXREAL_0:17;
hence |.x-x0.| < r1/2 by A74,XXREAL_0:2;
|.y-y0.| <= |. (x-x0) + (y-y0)*<i> .| by Lm16;
then
A76: |.y-y0.| < r0 by A4,A73,XXREAL_0:2;
hence |.y-y0.| < r1/2 by A75,XXREAL_0:2;
A77: r0 <=r2/2 by XXREAL_0:17;
hence |.x-x0.| < r2/2 by A74,XXREAL_0:2;
thus |.y-y0.| < r2/2 by A77,A76,XXREAL_0:2;
end;
reconsider N as Neighbourhood of z0 by A17,A36,CFDIFF_1:6,XXREAL_0:21;
now
let z be object;
assume
A78: z in N;
then reconsider zz=z as Complex;
set x=Re zz, y=Im zz;
x+y*<i> in N by A78,COMPLEX1:13;
then |.x-x0.| < r2/2 & |.y-y0.| < r2/2 by A72;
then
A79: |.x-x0.| + |.y-y0.| < r2/2+r2/2 by XREAL_1:8;
<*x,y*> in REAL 2 by FINSEQ_2:101;
then reconsider xy=<*x,y*> as Point of REAL-NS 2 by REAL_NS1:def 4;
xy-gvxy0 = <* x-x0,y-y0 *> by A5,A20,Lm10;
then ||.xy-gvxy0.|| <=|.x-x0.| + |.y-y0.| by Lm17;
then ||.xy-gvxy0.|| < r2 by A79,XXREAL_0:2;
then xy in {wxy where wxy is Point of REAL-NS 2 : ||.wxy-gvxy0.|| < r2 };
then
A80: <*x,y *> in Nv by A37;
rng v c= dom (proj(1,1)qua Function") by PDIFF_1:2;
then z=x+y*<i> & dom <>*v = dom v by COMPLEX1:13,RELAT_1:27;
hence z in dom f by A1,A19,A34,A80;
end;
then
A81: N c= dom f by TARSKI:def 3;
defpred R0[Complex, Complex] means $2 = proj(1,1).(Ru.
<* Re $1, Im $1 *>) + (proj(1,1).(Rv.<* Re $1, Im $1 *>))*<i>;
reconsider a = (partdiff(u,xy0,1)+<i>*partdiff(v,xy0,1))
as Element of COMPLEX by XCMPLX_0:def 2;
deffunc L0(Complex) = In(a* $1,COMPLEX);
consider L be Function of COMPLEX,COMPLEX such that
A82: for x be Element of COMPLEX holds L.x= L0(x) from FUNCT_2:sch 4;
for z be Complex holds L/.z = a*z
proof let z be Complex;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
L/.z= L0(z) by A82;
hence thesis;
end;
then reconsider L as C_LinearFunc by CFDIFF_1:def 4;
A83: now
let z be Element of COMPLEX;
reconsider y = proj(1,1).(Ru.<* Re z, Im z *>) + (proj(1,1).(Rv.<* Re z,
Im z *>))*<i> as Element of COMPLEX by XCMPLX_0:def 2;
take y;
thus R0[z,y];
end;
consider R be Function of COMPLEX,COMPLEX such that
A84: for z be Element of COMPLEX holds R0[z, R.z] from FUNCT_2:sch 3(A83);
for h be 0-convergent non-zero Complex_Sequence holds (h")(#)(R/*h) is
convergent & lim ((h")(#)(R/*h)) = 0
proof
let h be 0-convergent non-zero Complex_Sequence;
A85: now
let r be Real;
assume
A86: 0 < r;
Rv is total by NDIFF_1:def 5;
then consider d2 be Real such that
A87: d2 > 0 and
A88: for z be Point of REAL-NS 2 st z <> 0.(REAL-NS 2) & ||.z.|| <
d2 holds ||.z.||" * ||. Rv/.z .|| < r/2 by A86,NDIFF_1:23;
Ru is total by NDIFF_1:def 5;
then consider d1 be Real such that
A89: d1 > 0 and
A90: for z be Point of REAL-NS 2 st z <> 0.(REAL-NS 2) & ||.z.|| <
d1 holds ||.z.||" * ||. Ru/.z .|| < r/2 by A86,NDIFF_1:23;
set d = min(d1,d2);
lim h = 0 & 0 < d by A89,A87,CFDIFF_1:def 1,XXREAL_0:21;
then consider M be Nat such that
A91: for n be Nat st M<=n holds |. h.n-0 .| < d by COMSEQ_2:def 6;
A92: d <=d2 by XXREAL_0:17;
A93: d <= d1 by XXREAL_0:17;
now
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
set x = Re (h.nn), y = Im (h.nn);
<*x,y*> in REAL 2 by FINSEQ_2:101;
then reconsider z=<*x,y*> as Point of REAL-NS 2 by REAL_NS1:def 4;
A94: z <> 0.(REAL-NS 2)
proof
assume z = 0.(REAL-NS 2);
then z = 0*2 by REAL_NS1:def 4
.= <* 0,0 *> by EUCLID:54,70;
then x=0 & y=0 by FINSEQ_1:77;
then h.nn = 0 by COMPLEX1:4;
hence contradiction by COMSEQ_1:4;
end;
h.nn <> 0 by COMSEQ_1:4;
then
A95: 0 < |.h.n.| by COMPLEX1:47;
R/.(h.n) = proj(1,1).(Ru.<* Re (h.n), Im (h.n) *>) + (proj(1,1).
(Rv.<* Re (h.nn), Im (h.nn) *>))*<i> by A84;
then
A96: |.h.n.|"* |. R/.(h.n) .| <= |.h.n.|"* (|.proj(1,1).(Ru.<* Re (
h.n), Im (h.n) *>).| + |.proj(1,1).(Rv.<* Re (h.n), Im (h.n) *>).|)
by
A95,Lm15,XREAL_1:64;
Ru is total by NDIFF_1:def 5;
then dom Ru = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then
A97: |.proj(1,1).(Ru.<* Re (h.n), Im (h.n) *>).| = |.proj(1,1).(Ru
/.z ).| by PARTFUN1:def 6
.= ||. Ru/.z .|| by Lm21;
Rv is total by NDIFF_1:def 5;
then dom Rv = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then
A98: |.proj(1,1).(Rv.<* Re (h.n), Im (h.n) *>).| = |.proj(1,1).(Rv
/.z ).| by PARTFUN1:def 6
.= ||. Rv/.z .|| by Lm21;
h.n = x+y*<i> by COMPLEX1:13;
then
A99: ||.z.|| = |.h.n.| by Lm14;
assume M <= n;
then
A100: |. h.n-0 .| < d by A91;
then ||.z.|| < d2 by A92,A99,XXREAL_0:2;
then
A101: ||.z.||"* ||. Rv/.z .|| < r/2 by A88,A94;
||.z.|| < d1 by A93,A100,A99,XXREAL_0:2;
then ||.z.||"* ||. Ru/.z .|| < r/2 by A90,A94;
then |.h.n.|"* |.proj(1,1).(Ru.<* Re (h.n), Im (h.n) *>).| + |.h.n.|
"* |.proj(1,1).(Rv.<* Re (h.n), Im (h.n) *>).| < r/2 +r/2 by A99,A101
,A97,A98,XREAL_1:8;
then |.h.n.|"* |. R/.(h.n) .| < r by A96,XXREAL_0:2;
then |.(h.n)".|* |. R/.(h.n) .| < r by COMPLEX1:66;
then
A102: |.(h.n)"* (R/.(h.n)) .| < r by COMPLEX1:65;
dom R = COMPLEX by FUNCT_2:def 1;
then rng h c= dom R;
then |. (h.nn)"*((R/*h).nn) .| < r by A102,FUNCT_2:109;
then |. (h".n)*((R/*h).n) .| < r by VALUED_1:10;
hence |.((h")(#)(R/*h)).n-0 .| < r by VALUED_1:5;
end;
hence ex M be Nat st for n be Nat st M <= n holds
|.((h")(#)(R/*h)).n-0c .| < r;
end;
then (h")(#)(R/*h) is convergent by COMSEQ_2:def 5;
hence thesis by A85,COMSEQ_2:def 6;
end;
then reconsider R as C_RestFunc by CFDIFF_1:def 3;
now
let z be Complex;
set x = Re z, y = Im z;
A103: z = x+y*<i> by COMPLEX1:13;
then
A104: z-z0 = (x-x0)+(y-y0)*<i> by A4;
then Re (z-z0)=x-x0 by COMPLEX1:12;
then
A105: <* Re(z-z0), Im(z-z0) *> = <* x-x0, y-y0 *> by A104,COMPLEX1:12;
A106: z-z0 in COMPLEX by XCMPLX_0:def 2;
assume z in N;
hence f/.z - f/.z0
= (partdiff(u,xy0,1)+<i>*partdiff(v,xy0,1))*((x-x0)+(y-y0)*<i>)
+ (proj(1,1).(Ru.<*x-x0,y-y0*>)
+ (proj(1,1).(Rv.<*x-x0,y-y0*>))*<i>)
by A4,A50,A103
.= L0(z-z0)
+ (proj(1,1).(Ru.<*x-x0,y-y0*>)
+ (proj(1,1).(Rv.<*x-x0,y-y0*>))*<i>)
by A4,A103
.= L/.(z-z0) + (proj(1,1).(Ru.<*x-x0,y-y0*>) +
(proj(1,1).(Rv.<*x-x0,y-y0*>))*<i>) by A82,A106
.= L/.(z-z0) + R/.(z-z0) by A84,A105,A106;
end;
then f is_differentiable_in z0 by A81,CFDIFF_1:def 6;
hence thesis by A2,A3,A4,A5,Th2;
end;