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; :: 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 x00, y00 be Real; :: thesis: for xy0 being Element of REAL 2 st xy0 = <*x00,y00*> & <>* 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 = <*x00,y00*> & <>* 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 = <*x00,y00*> 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*> )
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)) " ;
consider g being PartFunc of (REAL-NS 2),(REAL-NS 1), gxy0 being 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 being RestFunc 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 A6, NDIFF_1:def 7;
consider R being RestFunc of (REAL-NS 2),(REAL-NS 1) such that
A9: 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 A8;
consider r0 being 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 being PartFunc of (REAL-NS 2),(REAL-NS 1), fxy0 being 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 ((proj (1,1)) ") by PDIFF_1:2;
then A14: dom (<>* u) = dom u by RELAT_1:27;
A15: 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
A16: xy in N and
A17: z = xy - xy0 and
A18: <*L1*> = (diff ((<>* u),xy0)) . z and
A19: <*R1*> = R . z ; :: thesis: (u . xy) - (u . xy0) = L1 + R1
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 ;
:: thesis: verum
end;
set Nx0 = ].(x0 - r0),(x0 + r0).[;
reconsider Nx0 = ].(x0 - r0),(x0 + r0).[ as Neighbourhood of x0 by A10, RCOMP_1:def 6;
A27: 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 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 ; :: thesis: <*x,y0*> in N
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 <*x,y0*> in N by A11; :: thesis: verum
end;
now :: thesis: for s being object st s in (reproj (1,xy0)) .: Nx0 holds
s in dom u
let s be object ; :: thesis: ( s in (reproj (1,xy0)) .: Nx0 implies s in dom u )
assume s in (reproj (1,xy0)) .: Nx0 ; :: thesis: s in dom u
then consider x being Element of REAL such that
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; :: 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 A34: 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 );
A35: now :: thesis: for x being Element of REAL ex y being Element of REAL st S1[x,y]
let x be Element of REAL ; :: thesis: ex y being Element of REAL st S1[x,y]
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 = y; :: thesis: S1[x,y]
thus S1[x,y] by A37; :: thesis: verum
end;
consider R1 being Function of REAL,REAL such that
A38: for x being Element of REAL holds S1[x,R1 . x] from FUNCT_2:sch 3(A35);
A39: now :: thesis: for x being Real
for vx being Element of REAL 2 st vx = <*x,0*> holds
<*(R1 . x)*> = R . vx
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 A40: vx = <*x,0*> ; :: thesis: <*(R1 . x)*> = R . vx
x in REAL by XREAL_0:def 1;
then ex vx1 being Element of REAL 2 st
( vx1 = <*x,0*> & <*(R1 . x)*> = R . vx1 ) by A38;
hence <*(R1 . x)*> = R . vx by A40; :: thesis: verum
end;
for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 )
defpred S2[ Nat, Element of (REAL-NS 2)] means $2 = <*(h . $1),0*>;
A41: now :: thesis: for n being Element of NAT ex y being Element of (REAL-NS 2) st S2[n,y]
let n be Element of NAT ; :: thesis: ex y being Element of (REAL-NS 2) st S2[n,y]
<*(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 = y; :: thesis: S2[n,y]
thus S2[n,y] ; :: thesis: verum
end;
consider h1 being sequence of (REAL-NS 2) such that
A42: for n being Element of NAT holds S2[n,h1 . n] from FUNCT_2:sch 3(A41);
 A43: for n being Nat holds S2[n,h1 . n]
proof
let n be Nat; :: thesis: S2[n,h1 . n]
n in NAT by ORDINAL1:def 12;
hence S2[n,h1 . n] by A42; :: thesis: verum
end;
reconsider h1 = h1 as sequence of (REAL-NS 2) ;
now :: thesis: for n being Element of NAT holds ||.h1.|| . n = (abs h) . n
let n be Element of NAT ; :: thesis: ||.h1.|| . n = (abs h) . n
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 ; :: thesis: verum
end;
then A45: ||.h1.|| = abs h by FUNCT_2:63;
set g = (||.h1.|| ") (#) (R /* h1);
now :: thesis: for n being Element of NAT holds ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R1 /* h))) . n
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 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 ||.((||.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
.= ||.((|.(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 ; :: thesis: verum
end;
then A52: abs ((h ") (#) (R1 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).|| by FUNCT_2:63;
now :: thesis: for n being Nat holds h1 . n <> 0. (REAL-NS 2)
let n be Nat; :: thesis: h1 . n <> 0. (REAL-NS 2)
A53: h . n <> 0 by SEQ_1:5;
A54: h1 . n = <*(h . n),0*> by A43;
now :: thesis: not h1 . n = 0. (REAL-NS 2)
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 A54, A53, FINSEQ_1:77; :: thesis: verum
end;
hence h1 . n <> 0. (REAL-NS 2) ; :: thesis: verum
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 & h1 is 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 ( ||.((||.h1.|| ") (#) (R /* h1)).|| is convergent & lim ||.((||.h1.|| ") (#) (R /* h1)).|| = 0 ) by Th4;
hence ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by A52, Th3; :: thesis: verum
end;
then reconsider R1 = 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 being Element of REAL such that
A56: <*Dux*> = (diff ((<>* u),xy0)) . ex0 by FINSEQ_2:97;
deffunc H1( Real) -> Element of REAL = In ((Dux * $1),REAL);
consider LD1 being Function of REAL,REAL such that
A57: for x being Element of REAL holds LD1 . x = H1(x) from FUNCT_2:sch 4();
 A58: for x being Real holds LD1 . x = Dux * x
proof
let x be Real; :: thesis: LD1 . x = Dux * x
reconsider x = x as Element of REAL by XREAL_0:def 1;
LD1 . x = H1(x) by A57;
hence LD1 . x = Dux * x ; :: thesis: verum
end;
set Ny0 = ].(y0 - r0),(y0 + r0).[;
reconsider Ny0 = ].(y0 - r0),(y0 + r0).[ as Neighbourhood of y0 by A10, RCOMP_1:def 6;
A59: 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 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 ; :: thesis: <*x0,y*> in N
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 <*x0,y*> in N by A11; :: thesis: verum
end;
now :: thesis: for s being object st s in (reproj (2,xy0)) .: Ny0 holds
s in dom u
let s be object ; :: thesis: ( s in (reproj (2,xy0)) .: Ny0 implies s in dom u )
assume s in (reproj (2,xy0)) .: Ny0 ; :: thesis: s in dom u
then consider y being Element of REAL such that
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; :: 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 A66: 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 );
A67: now :: thesis: for x being Element of REAL ex y being Element of REAL st S2[x,y]
let x be Element of REAL ; :: thesis: ex y being Element of REAL st S2[x,y]
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 = y; :: thesis: S2[x,y]
thus S2[x,y] by A69; :: thesis: verum
end;
consider R3 being Function of REAL,REAL such that
A70: for x being Element of REAL holds S2[x,R3 . x] from FUNCT_2:sch 3(A67);
A71: now :: thesis: for y being Real
for vy being Element of REAL 2 st vy = <*0,y*> holds
<*(R3 . y)*> = R . vy
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 )
reconsider yy = y as Element of REAL by XREAL_0:def 1;
assume A72: vy = <*0,y*> ; :: thesis: <*(R3 . y)*> = R . vy
ex vy1 being Element of REAL 2 st
( vy1 = <*0,y*> & <*(R3 . yy)*> = R . vy1 ) by A70;
hence <*(R3 . y)*> = R . vy by A72; :: thesis: verum
end;
for h being non-zero 0 -convergent Real_Sequence holds
( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )
proof
let h be non-zero 0 -convergent Real_Sequence; :: thesis: ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 )
defpred S3[ Nat, Element of (REAL-NS 2)] means $2 = <*0,(h . $1)*>;
A73: now :: thesis: for n being Element of NAT ex y being Element of (REAL-NS 2) st S3[n,y]
let n be Element of NAT ; :: thesis: ex y being Element of (REAL-NS 2) st S3[n,y]
<*(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 = y; :: thesis: S3[n,y]
thus S3[n,y] ; :: thesis: verum
end;
consider h1 being sequence of (REAL-NS 2) such that
A74: for n being Element of NAT holds S3[n,h1 . n] from FUNCT_2:sch 3(A73);
 A75: for n being Nat holds S3[n,h1 . n]
proof
let n be Nat; :: thesis: S3[n,h1 . n]
n in NAT by ORDINAL1:def 12;
hence S3[n,h1 . n] by A74; :: thesis: verum
end;
reconsider h1 = h1 as sequence of (REAL-NS 2) ;
now :: thesis: for n being Element of NAT holds ||.h1.|| . n = (abs h) . n
let n be Element of NAT ; :: thesis: ||.h1.|| . n = (abs h) . n
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 ; :: thesis: verum
end;
then A77: ||.h1.|| = abs h by FUNCT_2:63;
set g = (||.h1.|| ") (#) (R /* h1);
now :: thesis: for n being Element of NAT holds ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R3 /* h))) . n
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 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 ||.((||.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
.= ||.((|.(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 ; :: thesis: verum
end;
then A84: abs ((h ") (#) (R3 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).|| by FUNCT_2:63;
now :: thesis: for n being Nat holds h1 . n <> 0. (REAL-NS 2)
let n be Nat; :: thesis: h1 . n <> 0. (REAL-NS 2)
A85: h . n <> 0 by SEQ_1:5;
A86: h1 . n = <*0,(h . n)*> by A75;
now :: thesis: not h1 . n = 0. (REAL-NS 2)
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 A86, A85, FINSEQ_1:77; :: thesis: verum
end;
hence h1 . n <> 0. (REAL-NS 2) ; :: thesis: verum
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 & h1 is 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 ( ||.((||.h1.|| ") (#) (R /* h1)).|| is convergent & lim ||.((||.h1.|| ") (#) (R /* h1)).|| = 0 ) by Th4;
hence ( (h ") (#) (R3 /* h) is convergent & lim ((h ") (#) (R3 /* h)) = 0 ) by A84, Th3; :: thesis: verum
end;
then reconsider R3 = 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 being Element of REAL such that
A88: <*Duy*> = (diff ((<>* u),xy0)) . ey0 by FINSEQ_2:97;
deffunc H2( Real) -> Element of REAL = In ((Duy * $1),REAL);
consider LD3 being Function of REAL,REAL such that
A89: for x being Element of REAL holds LD3 . x = H2(x) from FUNCT_2:sch 4();
 A90: for x being Real holds LD3 . x = Duy * x
proof
let x be Real; :: thesis: LD3 . x = Duy * x
reconsider x = x as Element of REAL by XREAL_0:def 1;
LD3 . x = H2(x) by A89;
hence LD3 . x = Duy * x ; :: thesis: verum
end;
reconsider LD3 = LD3 as LinearFunc by A90, FDIFF_1:def 3;
A91: LD3 . 1 = Duy * 1 by A90
.= Duy ;
A92: for y being Element of REAL holds (u * (reproj (2,xy0))) . y = u . <*x0,y*>
proof
let y be Element of 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 A3, FINSEQ_7:14 ;
:: thesis: verum
end;
A93: 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 A94: y in Ny0 ; :: thesis: ((u * (reproj (2,xy0))) . y) - ((u * (reproj (2,xy0))) . y0) = (LD3 . (y - y0)) + (R3 . (y - y0))
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 ; :: thesis: verum
end;
reconsider LD1 = LD1 as LinearFunc by A58, FDIFF_1:def 3;
A100: LD1 . 1 = Dux * 1 by A58
.= Dux ;
A101: for x being Element of REAL holds (u * (reproj (1,xy0))) . x = u . <*x,y0*>
proof
let x be Element of REAL ; :: thesis: (u * (reproj (1,xy0))) . x = u . <*x,y0*>
x in REAL ;
then x in dom (reproj (1,xy0)) by PDIFF_1:def 5;
hence (u * (reproj (1,xy0))) . x = u . ((reproj (1,xy0)) . x) by FUNCT_1:13
.= u . (Replace (xy0,1,x)) by PDIFF_1:def 5
.= u . <*x,y0*> by A3, FINSEQ_7:13 ;
:: thesis: verum
end;
A102: 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 A103: x in Nx0 ; :: thesis: ((u * (reproj (1,xy0))) . x) - ((u * (reproj (1,xy0))) . x0) = (LD1 . (x - x0)) + (R1 . (x - x0))
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 ; :: thesis: verum
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 ( 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 A111, A109, A56, A88, A102, A93, A100, A34, A91, A66, A110, FDIFF_1:def 5; :: thesis: verum