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

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

then A34: Nx0 c= dom (u * (reproj (1,xy0))) by FUNCT_3:3;

defpred S_{1}[ Element of REAL , Element of REAL ] means ex vx being Element of REAL 2 st

( vx = <*$1,0*> & <*$2*> = R . vx );

A38: for x being Element of REAL holds S_{1}[x,R1 . x]
from FUNCT_2:sch 3(A35);

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

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

A58: for x being Real holds LD1 . x = Dux * x

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

then A66: Ny0 c= dom (u * (reproj (2,xy0))) by FUNCT_3:3;

defpred S_{2}[ Element of REAL , Element of REAL ] means ex vy being Element of REAL 2 st

( vy = <*0,$1*> & <*$2*> = R . vy );

A70: for x being Element of REAL holds S_{2}[x,R3 . x]
from FUNCT_2:sch 3(A67);

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

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

A90: for x being Real holds LD3 . x = Duy * x

A91: LD3 . 1 = Duy * 1 by A90

.= Duy ;

A92: for y being Element of REAL holds (u * (reproj (2,xy0))) . y = u . <*x0,y*>

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

A100: LD1 . 1 = Dux * 1 by A58

.= Dux ;

A101: for x being Element of REAL holds (u * (reproj (1,xy0))) . x = u . <*x,y0*>

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

.= 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

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

set Nx0 = ].(x0 - r0),(x0 + r0).[;
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;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

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

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

s in dom u

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

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

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

then consider x being Element of REAL such that

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

then A34: Nx0 c= dom (u * (reproj (1,xy0))) by FUNCT_3:3;

defpred S

( vx = <*$1,0*> & <*$2*> = R . vx );

A35: now :: thesis: for x being Element of REAL ex y being Element of REAL st S_{1}[x,y]

consider R1 being Function of REAL,REAL such that let x be Element of REAL ; :: thesis: ex y being Element of REAL st S_{1}[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: S_{1}[x,y]

thus S_{1}[x,y]
by A37; :: thesis: verum

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

thus S

A38: for x being Element of REAL holds S

A39: now :: thesis: for x being Real

for vx being Element of REAL 2 st vx = <*x,0*> holds

<*(R1 . x)*> = R . vx

for h being non-zero 0 -convergent Real_Sequence holds 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;<*(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

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

proof

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

defpred S_{2}[ Nat, Element of (REAL-NS 2)] means $2 = <*(h . $1),0*>;

A42: for n being Element of NAT holds S_{2}[n,h1 . n]
from FUNCT_2:sch 3(A41);

A43: for n being Nat holds S_{2}[n,h1 . n]

set g = (||.h1.|| ") (#) (R /* h1);

( 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;defpred S

A41: now :: thesis: for n being Element of NAT ex y being Element of (REAL-NS 2) st S_{2}[n,y]

consider h1 being sequence of (REAL-NS 2) such that let n be Element of NAT ; :: thesis: ex y being Element of (REAL-NS 2) st S_{2}[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: S_{2}[n,y]

thus S_{2}[n,y]
; :: thesis: verum

end;<*(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: S

thus S

A42: for n being Element of NAT holds S

A43: for n being Nat holds S

proof

reconsider h1 = h1 as sequence of (REAL-NS 2) ;
let n be Nat; :: thesis: S_{2}[n,h1 . n]

n in NAT by ORDINAL1:def 12;

hence S_{2}[n,h1 . n]
by A42; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence S

now :: thesis: for n being Element of NAT holds ||.h1.|| . n = (abs h) . n

then A45:
||.h1.|| = abs h
by FUNCT_2:63;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;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

set g = (||.h1.|| ") (#) (R /* h1);

now :: thesis: for n being Element of NAT holds ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R1 /* h))) . n

then A52:
abs ((h ") (#) (R1 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).||
by FUNCT_2:63;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;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

now :: thesis: for n being Nat holds h1 . n <> 0. (REAL-NS 2)

then A55:
h1 is non-zero
by NDIFF_1:7;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;

end;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)

hence
h1 . n <> 0. (REAL-NS 2)
; :: thesis: verumassume
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;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

( 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

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 H

consider LD1 being Function of REAL,REAL such that

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

A58: for x being Real holds LD1 . x = Dux * x

proof

set Ny0 = ].(y0 - r0),(y0 + r0).[;
let x be Real; :: thesis: LD1 . x = Dux * x

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

LD1 . x = H_{1}(x)
by A57;

hence LD1 . x = Dux * x ; :: thesis: verum

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

LD1 . x = H

hence LD1 . x = Dux * x ; :: thesis: verum

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

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

s in dom u

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

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

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

then consider y being Element of REAL such that

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

then A66: Ny0 c= dom (u * (reproj (2,xy0))) by FUNCT_3:3;

defpred S

( vy = <*0,$1*> & <*$2*> = R . vy );

A67: now :: thesis: for x being Element of REAL ex y being Element of REAL st S_{2}[x,y]

consider R3 being Function of REAL,REAL such that let x be Element of REAL ; :: thesis: ex y being Element of REAL st S_{2}[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: S_{2}[x,y]

thus S_{2}[x,y]
by A69; :: thesis: verum

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

thus S

A70: for x being Element of REAL holds S

A71: now :: thesis: for y being Real

for vy being Element of REAL 2 st vy = <*0,y*> holds

<*(R3 . y)*> = R . vy

for h being non-zero 0 -convergent Real_Sequence holds 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;<*(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

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

proof

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

defpred S_{3}[ Nat, Element of (REAL-NS 2)] means $2 = <*0,(h . $1)*>;

A74: for n being Element of NAT holds S_{3}[n,h1 . n]
from FUNCT_2:sch 3(A73);

A75: for n being Nat holds S_{3}[n,h1 . n]

set g = (||.h1.|| ") (#) (R /* h1);

( 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;defpred S

A73: now :: thesis: for n being Element of NAT ex y being Element of (REAL-NS 2) st S_{3}[n,y]

consider h1 being sequence of (REAL-NS 2) such that let n be Element of NAT ; :: thesis: ex y being Element of (REAL-NS 2) st S_{3}[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: S_{3}[n,y]

thus S_{3}[n,y]
; :: thesis: verum

end;<*(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: S

thus S

A74: for n being Element of NAT holds S

A75: for n being Nat holds S

proof

reconsider h1 = h1 as sequence of (REAL-NS 2) ;
let n be Nat; :: thesis: S_{3}[n,h1 . n]

n in NAT by ORDINAL1:def 12;

hence S_{3}[n,h1 . n]
by A74; :: thesis: verum

end;n in NAT by ORDINAL1:def 12;

hence S

now :: thesis: for n being Element of NAT holds ||.h1.|| . n = (abs h) . n

then A77:
||.h1.|| = abs h
by FUNCT_2:63;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;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

set g = (||.h1.|| ") (#) (R /* h1);

now :: thesis: for n being Element of NAT holds ||.((||.h1.|| ") (#) (R /* h1)).|| . n = (abs ((h ") (#) (R3 /* h))) . n

then A84:
abs ((h ") (#) (R3 /* h)) = ||.((||.h1.|| ") (#) (R /* h1)).||
by FUNCT_2:63;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;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

now :: thesis: for n being Nat holds h1 . n <> 0. (REAL-NS 2)

then A87:
h1 is non-zero
by NDIFF_1:7;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;

end;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)

hence
h1 . n <> 0. (REAL-NS 2)
; :: thesis: verumassume
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;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

( 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

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 H

consider LD3 being Function of REAL,REAL such that

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

A90: for x being Real holds LD3 . x = Duy * x

proof

reconsider LD3 = LD3 as LinearFunc by A90, FDIFF_1:def 3;
let x be Real; :: thesis: LD3 . x = Duy * x

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

LD3 . x = H_{2}(x)
by A89;

hence LD3 . x = Duy * x ; :: thesis: verum

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

LD3 . x = H

hence LD3 . x = Duy * x ; :: thesis: verum

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

A93:
for y being Real st y in Ny0 holds
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;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

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

proof

reconsider LD1 = LD1 as LinearFunc by A58, FDIFF_1:def 3;
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;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

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

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

x in REAL ;

then x in dom (reproj (1,xy0)) by PDIFF_1:def 5;

hence (u * (reproj (1,xy0))) . x = u . ((reproj (1,xy0)) . x) by FUNCT_1:13

.= u . (Replace (xy0,1,x)) by PDIFF_1:def 5

.= u . <*x,y0*> by A3, FINSEQ_7:13 ;

:: thesis: verum

end;x in REAL ;

then x in dom (reproj (1,xy0)) by PDIFF_1:def 5;

hence (u * (reproj (1,xy0))) . x = u . ((reproj (1,xy0)) . x) by FUNCT_1:13

.= u . (Replace (xy0,1,x)) by PDIFF_1:def 5

.= u . <*x,y0*> by A3, FINSEQ_7:13 ;

:: thesis: verum

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

proof

A109: (proj (2,2)) . xy0 =
xy0 . 2
by PDIFF_1:def 1
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;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

.= 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