let x0, y0 be Real; :: thesis:
let z be Element of REAL 2; :: thesis:
let f be PartFunc of (REAL 2),REAL ; :: thesis:
set r = partdiff f,z,1;
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,1 ; :: thesis:
consider x1, y1 being Real such that
A3: ( z = <*x1,y1*> & ex N being Neighbourhood of x1 st
( N c= dom (SVF1 1,f,z) & ex L being LINEAR ex R being REST st
( partdiff f,z,1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,f,z) . x) - ((SVF1 1,f,z) . x1) = (L . (x - x1)) + (R . (x - x1)) ) ) ) ) by A1, A2, Def12;
( x0 = x1 & y0 = y1 ) by A1, A3, FINSEQ_1:98;
then consider N being Neighbourhood of x0 such that
A4: ( N c= dom (SVF1 1,f,z) & ex L being LINEAR ex R being REST st
( partdiff f,z,1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,f,z) . x) - ((SVF1 1,f,z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) ) by A3;
consider L being LINEAR, R being REST such that
A5: ( partdiff f,z,1 = L . 1 & ( for x being Real st x in N holds
((SVF1 1,f,z) . x) - ((SVF1 1,f,z) . x0) = (L . (x - x0)) + (R . (x - x0)) ) ) by A4;
consider x2, y2 being Real such that
A6: ( z = <*x2,y2*> & SVF1 1,f,z is_differentiable_in x2 ) by A2, Def6;
consider N1 being Neighbourhood of x2 such that
A7: ( N1 c= dom (SVF1 1,f,z) & ex L being LINEAR ex R being REST st
( diff (SVF1 1,f,z),x2 = L . 1 & ( for x being Real st x in N1 holds
((SVF1 1,f,z) . x) - ((SVF1 1,f,z) . x2) = (L . (x - x2)) + (R . (x - x2)) ) ) ) by A6, FDIFF_1:def 6;
consider L1 being LINEAR, R1 being REST such that
A8: ( diff (SVF1 1,f,z),x2 = L1 . 1 & ( for x being Real st x in N1 holds
((SVF1 1,f,z) . x) - ((SVF1 1,f,z) . x2) = (L1 . (x - x2)) + (R1 . (x - x2)) ) ) by A7;
consider r1 being Real such that
A9: for p being Real holds L . p = r1 * p by FDIFF_1:def 4;
consider p1 being Real such that
A10: for p being Real holds L1 . p = p1 * p by FDIFF_1:def 4;
A11: partdiff f,z,1 = r1 * 1 by A5, A9;
A12: diff (SVF1 1,f,z),x2 = p1 * 1 by A8, A10;
A13: ( x0 = x2 & y0 = y2 ) by A1, A6, FINSEQ_1:98;

A14: now

let x be Real; :: thesis:
assume A15: ( x in N & x in N1 ) ; :: thesis:
then ((SVF1 1,f,z) . x) - ((SVF1 1,f,z) . x0) = (L . (x - x0)) + (R . (x - x0)) by A5;
then (L . (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A8, A13, A15;
then (r1 * (x - x0)) + (R . (x - x0)) = (L1 . (x - x0)) + (R1 . (x - x0)) by A9;
hence ((partdiff f,z,1) * (x - x0)) + (R . (x - x0)) = ((diff (SVF1 1,f,z),x2) * (x - x0)) + (R1 . (x - x0)) by A10, A11, A12; :: thesis:

end;

consider N0 being Neighbourhood of x0 such that
A16: ( N0 c= N & N0 c= N1 ) by A13, RCOMP_1:38;
consider g being real number such that
A17: ( 0 < g & N0 = ].(x0 - g),(x0 + g).[ ) by RCOMP_1:def 7;
deffunc H₁( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A18: for n being Element of NAT holds s1 . n = H₁(n) from SEQ_1:sch 1();

now

let n be Element of NAT ; :: thesis:
g / (n + 2) <> 0 by A17, XREAL_1:141;
hence s1 . n <> 0 by A18; :: thesis:

end;

then A19: s1 is non-zero by SEQ_1:7;
( s1 is convergent & lim s1 = 0 ) by A18, SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence by A19, FDIFF_1:def 1;
A20: for n being Element of NAT ex x being Real st
( x in N & x in N1 & h . n = x - x0 )

proof

let n be Element of NAT ; :: thesis:
A21: g / (n + 2) > 0 by A17, XREAL_1:141;
0 + 1 < (n + 1) + 1 by XREAL_1:8;
then g / (n + 2) < g / 1 by A17, XREAL_1:78;
then A22: x0 + (g / (n + 2)) < x0 + g by XREAL_1:8;
AA: x0 + (- g) < x0 + (g / (n + 2)) by A21, A17, XREAL_1:8;
A23: x0 + (g / (n + 2)) in ].(x0 - g),(x0 + g).[ by A22, AA;
take x = x0 + (g / (n + 2)); :: thesis:
thus ( x in N & x in N1 & h . n = x - x0 ) by A16, A17, A18, A23; :: thesis:

end;

A24: now

let n be Nat; :: thesis:
X: n in NAT by ORDINAL1:def 13;
then ex x being Real st
( x in N & x in N1 & h . n = x - x0 ) by A20;
then A25: ((partdiff f,z,1) * (h . n)) + (R . (h . n)) = ((diff (SVF1 1,f,z),x2) * (h . n)) + (R1 . (h . n)) by A14;
h is non-zero by FDIFF_1:def 1;
then A26: h . n <> 0 by SEQ_1:7, X;
A27: (((partdiff f,z,1) * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = (((diff (SVF1 1,f,z),x2) * (h . n)) + (R1 . (h . n))) / (h . n) by A25, XCMPLX_1:63;
A28: ((partdiff f,z,1) * (h . n)) / (h . n) = (partdiff f,z,1) * ((h . n) / (h . n)) by XCMPLX_1:75
.= (partdiff f,z,1) * 1 by A26, XCMPLX_1:60
.= partdiff f,z,1 ;
((diff (SVF1 1,f,z),x2) * (h . n)) / (h . n) = (diff (SVF1 1,f,z),x2) * ((h . n) / (h . n)) by XCMPLX_1:75
.= (diff (SVF1 1,f,z),x2) * 1 by A26, XCMPLX_1:60
.= diff (SVF1 1,f,z),x2 ;
then A29: (partdiff f,z,1) + ((R . (h . n)) / (h . n)) = (diff (SVF1 1,f,z),x2) + ((R1 . (h . n)) / (h . n)) by A27, A28, XCMPLX_1:63;
R is total by FDIFF_1:def 3;
then dom R = REAL by PARTFUN1:def 4;
then A30: rng h c= dom R ;
R1 is total by FDIFF_1:def 3;
then dom R1 = REAL by PARTFUN1:def 4;
then A31: rng h c= dom R1 ;
A32: (R . (h . n)) / (h . n) = (R . (h . n)) * ((h . n) " ) by XCMPLX_0:def 9
.= (R . (h . n)) * ((h " ) . n) by VALUED_1:10
.= ((R /* h) . n) * ((h " ) . n) by A30, FUNCT_2:185, X
.= ((h " ) (#) (R /* h)) . n by SEQ_1:12, X ;
(R1 . (h . n)) / (h . n) = (R1 . (h . n)) * ((h . n) " ) by XCMPLX_0:def 9
.= (R1 . (h . n)) * ((h " ) . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h " ) . n) by A31, FUNCT_2:185, X
.= ((h " ) (#) (R1 /* h)) . n by SEQ_1:12, X ;
then partdiff f,z,1 = (diff (SVF1 1,f,z),x2) + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n)) by A29, A32;
hence (partdiff f,z,1) - (diff (SVF1 1,f,z),x2) = (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n by RFUNCT_2:6, X; :: thesis:

end;

then A33: ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)) is constant by VALUED_0:def 18;
(((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1 = (partdiff f,z,1) - (diff (SVF1 1,f,z),x2) by A24;
then A34: lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) = (partdiff f,z,1) - (diff (SVF1 1,f,z),x2) by A33, SEQ_4:40;
A35: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 ) by FDIFF_1:def 3;
( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by FDIFF_1:def 3;
then (partdiff f,z,1) - (diff (SVF1 1,f,z),x2) = 0 - 0 by A34, A35, SEQ_2:26;
hence partdiff f,z,1 = diff (SVF1 1,f,z),x0 by A1, A6, FINSEQ_1:98; :: thesis: