reconsider ey0 = <*0,1*> as Point of (REAL-NS 2) by Lm10;
reconsider ex0 = <*1,0*> as Point of (REAL-NS 2) by Lm10;
let u be PartFunc of (REAL 2),REAL; :: thesis: for x0, y0 being Real
for xy0 being 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*> )
let x0, y0 be Real; :: thesis: for xy0 being 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*> )
let xy0 be Element of REAL 2; :: thesis: ( xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 implies ( 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*> ) )
assume that
A1: xy0 = <*x0,y0*> and
A2: <>* u is_differentiable_in xy0 ; :: thesis: ( 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*> )
set W = (proj (1,1)) " ;
consider g being PartFunc of (REAL-NS 2),(REAL-NS 1), gxy0 being Point of (REAL-NS 2) such that
A3: <>* u = g and
A4: xy0 = gxy0 and
A5: g is_differentiable_in gxy0 by A2, PDIFF_1:def 7;
consider N being Neighbourhood of gxy0 such that
A6: N c= dom g and
A7: ex R being REST of (REAL-NS 2),(REAL-NS 1) st
for xy being Point of (REAL-NS 2) st xy in N holds
(g /. xy) - (g /. gxy0) = ((diff (g,gxy0)) . (xy - gxy0)) + (R /. (xy - gxy0)) by A5, NDIFF_1:def 7;
consider R being REST of (REAL-NS 2),(REAL-NS 1) such that
A8: for xy being Point of (REAL-NS 2) st xy in N holds
(g /. xy) - (g /. gxy0) = ((diff (g,gxy0)) . (xy - gxy0)) + (R /. (xy - gxy0)) by A7;
consider r0 being Real such that
A9: 0 < r0 and
A10: { xy where xy is Point of (REAL-NS 2) : ||.(xy - gxy0).|| < r0 } c= N by NFCONT_1:def 1;
consider f being PartFunc of (REAL-NS 2),(REAL-NS 1), fxy0 being Point of (REAL-NS 2) such that
A11: ( <>* u = f & xy0 = fxy0 ) and
A12: diff ((<>* u),xy0) = diff (f,fxy0) by A2, PDIFF_1:def 8;
rng u c= dom ((proj (1,1)) ") by PDIFF_1:2;
then A13: dom (<>* u) = dom u by RELAT_1:27;
A14: for xy being Element of REAL 2
for L1, R1 being Real
for z being 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; :: thesis: for L1, R1 being Real
for z being 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
let L1, R1 be Real; :: thesis: for z being 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
let z be Element of REAL 2; :: thesis: ( xy in N & z = xy - xy0 & <*L1*> = (diff ((<>* u),xy0)) . z & <*R1*> = R . z implies (u . xy) - (u . xy0) = L1 + R1 )
assume that
A15: xy in N and
A16: z = xy - xy0 and
A17: <*L1*> = (diff ((<>* u),xy0)) . z and
A18: <*R1*> = R . z ; :: thesis: (u . xy) - (u . xy0) = L1 + R1
reconsider zxy = xy as Point of (REAL-NS 2) by REAL_NS1:def 4;
A19: zxy - gxy0 = z by A4, A16, 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 A18, A19, PARTFUN1:def 6;
then A20: ((diff (g,gxy0)) . (zxy - gxy0)) + (R /. (zxy - gxy0)) = <*(L1 + R1)*> by A3, A4, A11, A12, A17, A19, Lm7;
A21: xy0 in N by A4, NFCONT_1:4;
then A22: g /. gxy0 = g . xy0 by A4, A6, PARTFUN1:def 6
.= (<>* u) /. xy0 by A3, A6, A21, PARTFUN1:def 6 ;
A23: g /. zxy = g . xy by A6, A15, PARTFUN1:def 6
.= (<>* u) /. xy by A3, A6, A15, PARTFUN1:def 6 ;
A24: (g /. zxy) - (g /. gxy0) = ((diff (g,gxy0)) . (zxy - gxy0)) + (R /. (zxy - gxy0)) by A8, A15;
A25: (<>* u) /. xy0 = (<>* u) . xy0 by A3, A6, A21, PARTFUN1:def 6
.= <*(u . xy0)*> by A3, A6, A13, A21, Lm13 ;
(<>* u) /. xy = (<>* u) . xy by A3, A6, A15, PARTFUN1:def 6
.= <*(u . xy)*> by A3, A6, A13, A15, Lm13 ;
then (g /. zxy) - (g /. gxy0) = <*(u . xy)*> - <*(u . xy0)*> by A23, A22, A25, 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 A24, A20, FINSEQ_1:def 8
.= L1 + R1 by FINSEQ_1:def 8 ;
:: thesis: verum
end;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by A9, RCOMP_1:def 6;
A26: for x being Real st x in Nx0 holds
<*x,y0*> in N
proof
let x be Real; :: thesis: ( x in Nx0 implies <*x,y0*> in N )
reconsider xy = <*x,y0*> as Point of (REAL-NS 2) by Lm10;
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 ; :: thesis: <*x,y0*> in N
then A27: |.(x - x0).| < r0 by RCOMP_1:1;
xx1 `2 = 0 by FINSEQ_1:44;
then A28: abs (xx1 `2) = 0 by ABSVALUE:2;
xy - gxy0 = <*(x - x0),(y0 - y0)*> by A1, A4, Lm11
.= <*(x - x0),0*> ;
then A29: ||.(xy - gxy0).|| = |.xx.| by REAL_NS1:1;
( abs (xx1 `1) = |.(x - x0).| & |.xx.| <= (abs (xx1 `1)) + (abs (xx1 `2)) ) by FINSEQ_1:44, JGRAPH_1:31;
then ||.(xy - gxy0).|| < r0 by A27, A28, A29, XXREAL_0:2;
then xy in { z where z is Point of (REAL-NS 2) : ||.(z - gxy0).|| < r0 } ;
hence <*x,y0*> in N by A10; :: thesis: verum
end;
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
A30: x in Nx0 and
A31: s = (reproj (1,xy0)) . x by FUNCT_2:65;
A32: <*x,y0*> in N by A26, A30;
s = Replace (xy0,1,x) by A31, PDIFF_1:def 5
.= <*x,y0*> by A1, FINSEQ_7:13 ;
hence s in dom u by A3, A6, A13, A32; :: thesis: verum
end;
then ( dom (reproj (1,xy0)) = REAL & (reproj (1,xy0)) .: Nx0 c= dom u ) by FUNCT_2:def 1, TARSKI:def 3;
then A33: Nx0 c= dom (u * (reproj (1,xy0))) by FUNCT_3:3;
defpred S1[ Element of REAL , Element of REAL ] means ex vx being Element of REAL 2 st
( vx = <*$1,0*> & <*$2*> = R . vx );
A34: now
let x be Element of REAL ; :: thesis: ex y being Element of REAL st S1[x,y]
reconsider vx = <*x,0*> as Element of REAL 2 by FINSEQ_2:101;
R is total by NDIFF_1:def 5;
then A35: 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 A35, PARTFUN1:4;
then R . vx is Element of REAL 1 by REAL_NS1:def 4;
then consider y being Element of REAL such that
A36: <*y*> = R . vx by FINSEQ_2:97;
take y = y; :: thesis: S1[x,y]
thus S1[x,y] by A36; :: thesis: verum
end;
consider R1 being Function of REAL,REAL such that
A37: for x being Element of REAL holds S1[x,R1 . x] from FUNCT_2:sch 10(A34);
A38: now
let x be Real; :: thesis: for vx being Element of REAL 2 st vx = <*x,0*> holds
<*(R1 . x)*> = R . vx
let vx be Element of REAL 2; :: thesis: ( vx = <*x,0*> implies <*(R1 . x)*> = R . vx )
assume A39: vx = <*x,0*> ; :: thesis: <*(R1 . x)*> = R . vx
ex vx1 being Element of REAL 2 st
( vx1 = <*x,0*> & <*(R1 . x)*> = R . vx1 ) by A37;
hence <*(R1 . x)*> = R . vx by A39; :: thesis: verum
end;
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 )
defpred S2[ Element of NAT , Element of (REAL-NS 2)] means $2 = <*(h . $1),0*>;
A40: now
let n be Element of NAT ; :: thesis: ex y being Element of (REAL-NS 2) st S2[n,y]
<*(h . n),0*> in REAL 2 by FINSEQ_2:101;
then reconsider y = <*(h . n),0*> as Element of (REAL-NS 2) by REAL_NS1:def 4;
take y = y; :: thesis: S2[n,y]
thus S2[n,y] ; :: thesis: verum
end;
consider h1 being Function of NAT,(REAL-NS 2) such that
A41: for n being Element of NAT holds S2[n,h1 . n] from FUNCT_2:sch 10(A40);
 reconsider h1 = h1 as sequence of (REAL-NS 2) ;
now
let n be Element of NAT ; :: thesis: ||.h1.|| . n = (abs h) . n
A42: h1 . n = <*(h . n),0*> by A41;
thus ||.h1.|| . n = ||.(h1 . n).|| by NORMSP_0:def 4
.= abs (h . n) by A42, Lm19
.= (abs h) . n by VALUED_1:18 ; :: thesis: verum
end;
then A43: ||.h1.|| = abs h by FUNCT_2:63;
set g = (||.h1.|| ") (#) (R /* h1);
now
let n be Element of NAT ; :: thesis: ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R1 /* h))) . n
reconsider v = h1 . n as Element of REAL 2 by REAL_NS1:def 4;
dom R1 = REAL by PARTFUN1:def 2;
then A44: rng h c= dom R1 ;
A45: h1 . n = <*(h . n),0*> by A41;
R is total by NDIFF_1:def 5;
then A46: dom R = the carrier of (REAL-NS 2) by PARTFUN1:def 2;
then A47: rng h1 c= dom R ;
A48: h1 . n = <*(h . n),0*> by A41;
A49: R /. (h1 . n) = R . v by A46, PARTFUN1:def 6
.= <*(R1 . (h . n))*> by A38, A45 ;
thus ||.((||.h1.|| ") (#) (R /* h1)).|| . n = ||.(((||.h1.|| ") (#) (R /* h1)) . 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
.= ||.(((abs (h . n)) ") * ((R /* h1) . n)).|| by A48, Lm19
.= ||.(((abs (h . n)) ") * (R /. (h1 . n))).|| by A47, FUNCT_2:109
.= ||.((abs ((h . n) ")) * (R /. (h1 . n))).|| by COMPLEX1:66
.= (abs (abs ((h . n) "))) * ||.(R /. (h1 . n)).|| by NORMSP_1:def 1
.= (abs ((h . n) ")) * (abs (R1 . (h . n))) by A49, Lm21
.= abs (((h . n) ") * (R1 . (h . n))) by COMPLEX1:65
.= abs (((h . n) ") * ((R1 /* h) . n)) by A44, FUNCT_2:108
.= abs (((h ") . n) * ((R1 /* h) . n)) by VALUED_1:10
.= abs (((h ") (#) (R1 /* h)) . n) by VALUED_1:5
.= (abs ((h ") (#) (R1 /* h))) . n by VALUED_1:18 ; :: thesis: verum
end;
then A50: abs ((h ") (#) (R1 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).|| by FUNCT_2:63;
now
let n be Element of NAT ; :: thesis: h1 . n <> 0. (REAL-NS 2)
h is non-empty by FDIFF_1:def 1;
then A51: h . n <> 0 by SEQ_1:5;
A52: h1 . n = <*(h . n),0*> by A41;
now
assume h1 . n = 0. (REAL-NS 2) ; :: thesis: contradiction
then h1 . n = 0* 2 by REAL_NS1:def 4
.= <*0,0*> by EUCLID:54, EUCLID:70 ;
hence contradiction by A52, A51, FINSEQ_1:77; :: thesis: verum
end;
hence h1 . n <> 0. (REAL-NS 2) ; :: thesis: verum
end;
then A53: h1 is non-zero by NDIFF_1:7;
( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
then ( abs h is convergent & lim (abs h) = 0 ) by Th3;
then ( h1 is convergent & lim h1 = 0. (REAL-NS 2) ) by A43, Th4;
then h1 is convergent_to_0 by A53, NDIFF_1:def 4;
then ( (||.h1.|| ") (#) (R /* h1) is convergent & lim ((||.h1.|| ") (#) (R /* h1)) = 0. (REAL-NS 1) ) by NDIFF_1:def 5;
then ( ||.((||.h1.|| ") (#) (R /* h1)).|| is convergent & lim ||.((||.h1.|| ") (#) (R /* h1)).|| = 0 ) by Th4;
hence ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by A50, Th3; :: thesis: verum
end;
then reconsider R1 = R1 as REST 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 being Real such that
A54: <*Dux*> = (diff ((<>* u),xy0)) . ex0 by FINSEQ_2:97;
deffunc H1( Real) -> Element of REAL = Dux * $1;
consider LD1 being Function of REAL,REAL such that
A55: for x being Real holds LD1 . x = H1(x) from FUNCT_2:sch 4();
 set Ny0 = ].(y0 - r0),(y0 + r0).[;
reconsider Ny0 = ].(y0 - r0),(y0 + r0).[ as Neighbourhood of y0 by A9, RCOMP_1:def 6;
A56: for y being Real st y in Ny0 holds
<*x0,y*> in N
proof
let y be Real; :: thesis: ( y in Ny0 implies <*x0,y*> in N )
reconsider xy = <*x0,y*> as Point of (REAL-NS 2) by Lm10;
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 ; :: thesis: <*x0,y*> in N
then A57: |.(y - y0).| < r0 by RCOMP_1:1;
xx1 `1 = 0 by FINSEQ_1:44;
then A58: abs (xx1 `1) = 0 by ABSVALUE:2;
|.xx.| <= (abs (xx1 `1)) + (abs (xx1 `2)) by JGRAPH_1:31;
then A59: |.xx.| <= |.(y - y0).| by A58, FINSEQ_1:44;
xy - gxy0 = <*(x0 - x0),(y - y0)*> by A1, A4, Lm11
.= <*0,(y - y0)*> ;
then ||.(xy - gxy0).|| = |.xx.| by REAL_NS1:1;
then ||.(xy - gxy0).|| < r0 by A57, A59, XXREAL_0:2;
then xy in { z where z is Point of (REAL-NS 2) : ||.(z - gxy0).|| < r0 } ;
hence <*x0,y*> in N by A10; :: thesis: verum
end;
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
A60: y in Ny0 and
A61: s = (reproj (2,xy0)) . y by FUNCT_2:65;
A62: <*x0,y*> in N by A56, A60;
s = Replace (xy0,2,y) by A61, PDIFF_1:def 5
.= <*x0,y*> by A1, FINSEQ_7:14 ;
hence s in dom u by A3, A6, A13, A62; :: thesis: verum
end;
then ( dom (reproj (2,xy0)) = REAL & (reproj (2,xy0)) .: Ny0 c= dom u ) by FUNCT_2:def 1, TARSKI:def 3;
then A63: Ny0 c= dom (u * (reproj (2,xy0))) by FUNCT_3:3;
defpred S2[ Element of REAL , Element of REAL ] means ex vy being Element of REAL 2 st
( vy = <*0,$1*> & <*$2*> = R . vy );
A64: now
let x be Element of REAL ; :: thesis: ex y being Element of REAL st S2[x,y]
reconsider vx = <*0,x*> as Element of REAL 2 by FINSEQ_2:101;
R is total by NDIFF_1:def 5;
then A65: 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 A65, PARTFUN1:4;
then R . vx is Element of REAL 1 by REAL_NS1:def 4;
then consider y being Element of REAL such that
A66: <*y*> = R . vx by FINSEQ_2:97;
take y = y; :: thesis: S2[x,y]
thus S2[x,y] by A66; :: thesis: verum
end;
consider R3 being Function of REAL,REAL such that
A67: for x being Element of REAL holds S2[x,R3 . x] from FUNCT_2:sch 10(A64);
A68: now
let y be Real; :: thesis: for vy being Element of REAL 2 st vy = <*0,y*> holds
<*(R3 . y)*> = R . vy
let vy be Element of REAL 2; :: thesis: ( vy = <*0,y*> implies <*(R3 . y)*> = R . vy )
assume A69: vy = <*0,y*> ; :: thesis: <*(R3 . y)*> = R . vy
ex vy1 being Element of REAL 2 st
( vy1 = <*0,y*> & <*(R3 . y)*> = R . vy1 ) by A67;
hence <*(R3 . y)*> = R . vy by A69; :: thesis: verum
end;
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 )
defpred S3[ Element of NAT , Element of (REAL-NS 2)] means $2 = <*0,(h . $1)*>;
A70: now
let n be Element of NAT ; :: thesis: ex y being Element of (REAL-NS 2) st S3[n,y]
<*0,(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 = y; :: thesis: S3[n,y]
thus S3[n,y] ; :: thesis: verum
end;
consider h1 being Function of NAT,(REAL-NS 2) such that
A71: for n being Element of NAT holds S3[n,h1 . n] from FUNCT_2:sch 10(A70);
 reconsider h1 = h1 as sequence of (REAL-NS 2) ;
now
let n be Element of NAT ; :: thesis: ||.h1.|| . n = (abs h) . n
A72: h1 . n = <*0,(h . n)*> by A71;
thus ||.h1.|| . n = ||.(h1 . n).|| by NORMSP_0:def 4
.= abs (h . n) by A72, Lm20
.= (abs h) . n by VALUED_1:18 ; :: thesis: verum
end;
then A73: ||.h1.|| = abs h by FUNCT_2:63;
set g = (||.h1.|| ") (#) (R /* h1);
now
let n be Element of NAT ; :: thesis: ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R3 /* h))) . n
reconsider v = h1 . n as Element of REAL 2 by REAL_NS1:def 4;
dom R3 = REAL by PARTFUN1:def 2;
then A74: rng h c= dom R3 ;
A75: h1 . n = <*0,(h . n)*> by A71;
R is total by NDIFF_1:def 5;
then A76: dom R = the carrier of (REAL-NS 2) by PARTFUN1:def 2;
then A77: rng h1 c= dom R ;
A78: h1 . n = <*0,(h . n)*> by A71;
A79: R /. (h1 . n) = R . v by A76, PARTFUN1:def 6
.= <*(R3 . (h . n))*> by A68, A75 ;
thus ||.((||.h1.|| ") (#) (R /* h1)).|| . n = ||.(((||.h1.|| ") (#) (R /* h1)) . 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
.= ||.(((abs (h . n)) ") * ((R /* h1) . n)).|| by A78, Lm20
.= ||.(((abs (h . n)) ") * (R /. (h1 . n))).|| by A77, FUNCT_2:109
.= ||.((abs ((h . n) ")) * (R /. (h1 . n))).|| by COMPLEX1:66
.= (abs (abs ((h . n) "))) * ||.(R /. (h1 . n)).|| by NORMSP_1:def 1
.= (abs ((h . n) ")) * (abs (R3 . (h . n))) by A79, Lm21
.= abs (((h . n) ") * (R3 . (h . n))) by COMPLEX1:65
.= abs (((h . n) ") * ((R3 /* h) . n)) by A74, FUNCT_2:108
.= abs (((h ") . n) * ((R3 /* h) . n)) by VALUED_1:10
.= abs (((h ") (#) (R3 /* h)) . n) by VALUED_1:5
.= (abs ((h ") (#) (R3 /* h))) . n by VALUED_1:18 ; :: thesis: verum
end;
then A80: abs ((h ") (#) (R3 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).|| by FUNCT_2:63;
now
let n be Element of NAT ; :: thesis: h1 . n <> 0. (REAL-NS 2)
h is non-empty by FDIFF_1:def 1;
then A81: h . n <> 0 by SEQ_1:5;
A82: h1 . n = <*0,(h . n)*> by A71;
now
assume h1 . n = 0. (REAL-NS 2) ; :: thesis: contradiction
then h1 . n = 0* 2 by REAL_NS1:def 4
.= <*0,0*> by EUCLID:54, EUCLID:70 ;
hence contradiction by A82, A81, FINSEQ_1:77; :: thesis: verum
end;
hence h1 . n <> 0. (REAL-NS 2) ; :: thesis: verum
end;
then A83: h1 is non-zero by NDIFF_1:7;
( h is convergent & lim h = 0 ) by FDIFF_1:def 1;
then ( abs h is convergent & lim (abs h) = 0 ) by Th3;
then ( h1 is convergent & lim h1 = 0. (REAL-NS 2) ) by A73, Th4;
then h1 is convergent_to_0 by A83, NDIFF_1:def 4;
then ( (||.h1.|| ") (#) (R /* h1) is convergent & lim ((||.h1.|| ") (#) (R /* h1)) = 0. (REAL-NS 1) ) by NDIFF_1:def 5;
then ( ||.((||.h1.|| ") (#) (R /* h1)).|| is convergent & lim ||.((||.h1.|| ") (#) (R /* h1)).|| = 0 ) by Th4;
hence ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 ) by A80, Th3; :: thesis: verum
end;
then reconsider R3 = R3 as REST 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 being Real such that
A84: <*Duy*> = (diff ((<>* u),xy0)) . ey0 by FINSEQ_2:97;
deffunc H2( Real) -> Element of REAL = Duy * $1;
consider LD3 being Function of REAL,REAL such that
A85: for x being Real holds LD3 . x = H2(x) from FUNCT_2:sch 4();
 reconsider LD3 = LD3 as LINEAR by A85, FDIFF_1:def 3;
A86: LD3 . 1 = Duy * 1 by A85
.= Duy ;
A87: 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 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 A1, FINSEQ_7:14 ;
:: thesis: verum
end;
A88: for y being 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; :: thesis: ( y in Ny0 implies ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0)) )
assume A89: y in Ny0 ; :: thesis: ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0))
reconsider xy = <*x0,y*> as Element of REAL 2 by FINSEQ_2:101;
A90: LD3 . (y - y0) = Duy * (y - y0) by A85;
A91: xy - xy0 = <*(x0 - x0),(y - y0)*> by A1, Lm8
.= <*((y - y0) * 0),((y - y0) * 1)*>
.= (y - y0) * ey0 by Lm12 ;
A92: 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 A12, REAL_NS1:3
.= (diff ((<>* u),xy0)) . (xy - xy0) by A12, A91, A92, LOPBAN_1:def 5 ;
then A93: <*(LD3 . (y - y0))*> = (diff ((<>* u),xy0)) . (xy - xy0) by A84, A90, RVSUM_1:47;
<*0,(y - y0)*> = <*(x0 - x0),(y - y0)*>
.= xy - xy0 by A1, Lm8 ;
then A94: <*(R3 . (y - y0))*> = R . (xy - xy0) by A68;
thus ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (u . <*x0,y*>) - ((u * (reproj (2,xy0))) . y0) by A87
.= (u . xy) - (u . xy0) by A1, A87
.= (LD3 . (y - y0)) + (R3 . (y - y0)) by A14, A56, A89, A93, A94 ; :: thesis: verum
end;
reconsider LD1 = LD1 as LINEAR by A55, FDIFF_1:def 3;
A95: LD1 . 1 = Dux * 1 by A55
.= Dux ;
A96: 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:13
.= u . (Replace (xy0,1,x)) by PDIFF_1:def 5
.= u . <*x,y0*> by A1, FINSEQ_7:13 ;
:: thesis: verum
end;
A97: 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
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; :: thesis: ( x in Nx0 implies ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0)) )
assume A98: x in Nx0 ; :: thesis: ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))
reconsider xy = <*x,y0*> as Element of REAL 2 by FINSEQ_2:101;
A99: LD1 . (x - x0) = Dux * (x - x0) by A55;
A100: xy - xy0 = <*(x - x0),(y0 - y0)*> by A1, Lm8
.= <*((x - x0) * 1),((x - x0) * 0)*>
.= (x - x0) * ex0 by Lm12 ;
A101: 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 A12, REAL_NS1:3
.= (diff ((<>* u),xy0)) . (xy - xy0) by A12, A100, A101, LOPBAN_1:def 5 ;
then A102: <*(LD1 . (x - x0))*> = (diff ((<>* u),xy0)) . (xy - xy0) by A54, A99, RVSUM_1:47;
<*(x - x0),0*> = <*(x - x0),(y0 - y0)*>
.= xy - xy0 by A1, Lm8 ;
then A103: <*(R1 . (x - x0))*> = R . (xy - xy0) by A38;
thus ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (u . <*x,y0*>) - ((u * (reproj (1,xy0))) . x0) by A96
.= (u . xy) - (u . xy0) by A1, A96
.= (LD1 . (x - x0)) + (R1 . (x - x0)) by A14, A26, A98, A102, A103 ; :: thesis: verum
end;
A104: (proj (2,2)) . xy0 = xy0 . 2 by PDIFF_1:def 1
.= y0 by A1, FINSEQ_1:44 ;
then A105: u * (reproj (2,xy0)) is_differentiable_in (proj (2,2)) . xy0 by A88, A63, FDIFF_1:def 4;
A106: (proj (1,2)) . xy0 = xy0 . 1 by PDIFF_1:def 1
.= x0 by A1, FINSEQ_1:44 ;
then u * (reproj (1,xy0)) is_differentiable_in (proj (1,2)) . xy0 by A97, A33, FDIFF_1:def 4;
hence ( 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*> ) by A106, A104, A54, A84, A97, A88, A95, A33, A86, A63, A105, FDIFF_1:def 5, PDIFF_1:def 11; :: thesis: verum