let x0, y0 be Real; :: thesis: for z being Element of REAL 2
for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
partdiff f,z,2 = diff (SVF1 2,f,z),y0
let z be Element of REAL 2; :: thesis: for f being PartFunc of (REAL 2),REAL st z = <*x0,y0*> & f is_partial_differentiable_in z,2 holds
partdiff f,z,2 = diff (SVF1 2,f,z),y0
let f be PartFunc of (REAL 2),REAL ; :: thesis: ( z = <*x0,y0*> & f is_partial_differentiable_in z,2 implies partdiff f,z,2 = diff (SVF1 2,f,z),y0 )
set r = partdiff f,z,2;
assume that
A1: z = <*x0,y0*> and
A2: f is_partial_differentiable_in z,2 ; :: thesis: partdiff f,z,2 = diff (SVF1 2,f,z),y0
consider x1, y1 being Real such that
A3: z = <*x1,y1*> and
A4: ex N being Neighbourhood of y1 st
( N c= dom (SVF1 2,f,z) & ex L being LINEAR ex R being REST st
( partdiff f,z,2 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,f,z) . y) - ((SVF1 2,f,z) . y1) = (L . (y - y1)) + (R . (y - y1)) ) ) ) by A1, A2, Th12;
y0 = y1 by A1, A3, FINSEQ_1:98;
then consider N being Neighbourhood of y0 such that
N c= dom (SVF1 2,f,z) and
A5: ex L being LINEAR ex R being REST st
( partdiff f,z,2 = L . 1 & ( for y being Real st y in N holds
((SVF1 2,f,z) . y) - ((SVF1 2,f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) ) ) by A4;
consider L being LINEAR, R being REST such that
A6: partdiff f,z,2 = L . 1 and
A7: for y being Real st y in N holds
((SVF1 2,f,z) . y) - ((SVF1 2,f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) by A5;
consider r1 being Real such that
A8: for p being Real holds L . p = r1 * p by FDIFF_1:def 4;
A9: partdiff f,z,2 = r1 * 1 by A6, A8;
consider x2, y2 being Real such that
A10: z = <*x2,y2*> and
A11: SVF1 2,f,z is_differentiable_in y2 by A2, Th6;
consider N1 being Neighbourhood of y2 such that
N1 c= dom (SVF1 2,f,z) and
A12: ex L being LINEAR ex R being REST st
( diff (SVF1 2,f,z),y2 = L . 1 & ( for y being Real st y in N1 holds
((SVF1 2,f,z) . y) - ((SVF1 2,f,z) . y2) = (L . (y - y2)) + (R . (y - y2)) ) ) by A11, FDIFF_1:def 6;
consider L1 being LINEAR, R1 being REST such that
A13: diff (SVF1 2,f,z),y2 = L1 . 1 and
A14: for y being Real st y in N1 holds
((SVF1 2,f,z) . y) - ((SVF1 2,f,z) . y2) = (L1 . (y - y2)) + (R1 . (y - y2)) by A12;
consider p1 being Real such that
A15: for p being Real holds L1 . p = p1 * p by FDIFF_1:def 4;
A16: y0 = y2 by A1, A10, FINSEQ_1:98;
then consider N0 being Neighbourhood of y0 such that
A17: ( N0 c= N & N0 c= N1 ) by RCOMP_1:38;
consider g being real number such that
A18: 0 < g and
A19: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def 7;
deffunc H1( Element of NAT ) -> Element of REAL = g / ($1 + 2);
consider s1 being Real_Sequence such that
A20: for n being Element of NAT holds s1 . n = H1(n) from SEQ_1:sch 1();
now
let n be Element of NAT ; :: thesis: s1 . n <> 0
g / (n + 2) <> 0 by A18, XREAL_1:141;
hence s1 . n <> 0 by A20; :: thesis: verum
end;
then A21: s1 is non-empty by SEQ_1:7;
( s1 is convergent & lim s1 = 0 ) by A20, SEQ_4:46;
then reconsider h = s1 as convergent_to_0 Real_Sequence by A21, FDIFF_1:def 1;
A22: for n being Element of NAT ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
proof
let n be Element of NAT ; :: thesis: ex y being Real st
( y in N & y in N1 & h . n = y - y0 )
take y = y0 + (g / (n + 2)); :: thesis: ( y in N & y in N1 & h . n = y - y0 )
0 + 1 < (n + 1) + 1 by XREAL_1:8;
then g / (n + 2) < g / 1 by A18, XREAL_1:78;
then A23: y0 + (g / (n + 2)) < y0 + g by XREAL_1:8;
g / (n + 2) > 0 by A18, XREAL_1:141;
then y0 + (- g) < y0 + (g / (n + 2)) by A18, XREAL_1:8;
then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A23;
hence ( y in N & y in N1 & h . n = y - y0 ) by A17, A19, A20; :: thesis: verum
end;
A24: diff (SVF1 2,f,z),y2 = p1 * 1 by A13, A15;
A25: now
let y be Real; :: thesis: ( y in N & y in N1 implies ((partdiff f,z,2) * (y - y0)) + (R . (y - y0)) = ((diff (SVF1 2,f,z),y2) * (y - y0)) + (R1 . (y - y0)) )
assume that
A26: y in N and
A27: y in N1 ; :: thesis: ((partdiff f,z,2) * (y - y0)) + (R . (y - y0)) = ((diff (SVF1 2,f,z),y2) * (y - y0)) + (R1 . (y - y0))
((SVF1 2,f,z) . y) - ((SVF1 2,f,z) . y0) = (L . (y - y0)) + (R . (y - y0)) by A7, A26;
then (L . (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A14, A16, A27;
then (r1 * (y - y0)) + (R . (y - y0)) = (L1 . (y - y0)) + (R1 . (y - y0)) by A8;
hence ((partdiff f,z,2) * (y - y0)) + (R . (y - y0)) = ((diff (SVF1 2,f,z),y2) * (y - y0)) + (R1 . (y - y0)) by A15, A9, A24; :: thesis: verum
end;
now
R1 is total by FDIFF_1:def 3;
then dom R1 = REAL by PARTFUN1:def 4;
then A28: rng h c= dom R1 ;
let n be Nat; :: thesis: (partdiff f,z,2) - (diff (SVF1 2,f,z),y2) = (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n
R is total by FDIFF_1:def 3;
then dom R = REAL by PARTFUN1:def 4;
then A29: rng h c= dom R ;
A30: n in NAT by ORDINAL1:def 13;
then ex y being Real st
( y in N & y in N1 & h . n = y - y0 ) by A22;
then ((partdiff f,z,2) * (h . n)) + (R . (h . n)) = ((diff (SVF1 2,f,z),y2) * (h . n)) + (R1 . (h . n)) by A25;
then A31: (((partdiff f,z,2) * (h . n)) / (h . n)) + ((R . (h . n)) / (h . n)) = (((diff (SVF1 2,f,z),y2) * (h . n)) + (R1 . (h . n))) / (h . n) by XCMPLX_1:63;
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, A29, FUNCT_2:185
.= ((h " ) (#) (R /* h)) . n by A30, SEQ_1:12 ;
h is non-empty by FDIFF_1:def 1;
then A33: h . n <> 0 by A30, SEQ_1:7;
A34: (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 A30, A28, FUNCT_2:185
.= ((h " ) (#) (R1 /* h)) . n by A30, SEQ_1:12 ;
A35: ((diff (SVF1 2,f,z),y2) * (h . n)) / (h . n) = (diff (SVF1 2,f,z),y2) * ((h . n) / (h . n)) by XCMPLX_1:75
.= (diff (SVF1 2,f,z),y2) * 1 by A33, XCMPLX_1:60
.= diff (SVF1 2,f,z),y2 ;
((partdiff f,z,2) * (h . n)) / (h . n) = (partdiff f,z,2) * ((h . n) / (h . n)) by XCMPLX_1:75
.= (partdiff f,z,2) * 1 by A33, XCMPLX_1:60
.= partdiff f,z,2 ;
then (partdiff f,z,2) + ((R . (h . n)) / (h . n)) = (diff (SVF1 2,f,z),y2) + ((R1 . (h . n)) / (h . n)) by A31, A35, XCMPLX_1:63;
then partdiff f,z,2 = (diff (SVF1 2,f,z),y2) + ((((h " ) (#) (R1 /* h)) . n) - (((h " ) (#) (R /* h)) . n)) by A32, A34;
hence (partdiff f,z,2) - (diff (SVF1 2,f,z),y2) = (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . n by A30, RFUNCT_2:6; :: thesis: verum
end;
then ( ((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h)) is constant & (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) . 1 = (partdiff f,z,2) - (diff (SVF1 2,f,z),y2) ) by VALUED_0:def 18;
then A36: lim (((h " ) (#) (R1 /* h)) - ((h " ) (#) (R /* h))) = (partdiff f,z,2) - (diff (SVF1 2,f,z),y2) by SEQ_4:40;
A37: ( (h " ) (#) (R1 /* h) is convergent & lim ((h " ) (#) (R1 /* h)) = 0 ) by FDIFF_1:def 3;
( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 ) by FDIFF_1:def 3;
then (partdiff f,z,2) - (diff (SVF1 2,f,z),y2) = 0 - 0 by A36, A37, SEQ_2:26;
hence partdiff f,z,2 = diff (SVF1 2,f,z),y0 by A1, A10, FINSEQ_1:98; :: thesis: verum