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 LinearFunc ex R being RestFunc 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:77;

then consider N being Neighbourhood of y0 such that

N c= dom (SVF1 (2,f,z)) and

A5: ex L being LinearFunc ex R being RestFunc 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 LinearFunc, R being RestFunc 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 3;

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 LinearFunc ex R being RestFunc 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 5;

consider L1 being LinearFunc, R1 being RestFunc 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 3;

A16: y0 = y2 by A1, A10, FINSEQ_1:77;

then consider N0 being Neighbourhood of y0 such that

A17: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;

consider g being Real such that

A18: 0 < g and

A19: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def 6;

deffunc H_{1}( Nat) -> set = g / ($1 + 2);

consider s1 being Real_Sequence such that

A20: for n being Nat holds s1 . n = H_{1}(n)
from SEQ_1:sch 1();

( s1 is convergent & lim s1 = 0 ) by A20, SEQ_4:31;

then reconsider h = s1 as non-zero 0 -convergent 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 )

then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) by SEQ_4:25;

A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def 2;

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def 2;

then (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) = 0 - 0 by A36, A37, SEQ_2:12;

hence partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0) by A1, A10, FINSEQ_1:77; :: thesis: verum

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 LinearFunc ex R being RestFunc 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:77;

then consider N being Neighbourhood of y0 such that

N c= dom (SVF1 (2,f,z)) and

A5: ex L being LinearFunc ex R being RestFunc 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 LinearFunc, R being RestFunc 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 3;

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 LinearFunc ex R being RestFunc 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 5;

consider L1 being LinearFunc, R1 being RestFunc 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 3;

A16: y0 = y2 by A1, A10, FINSEQ_1:77;

then consider N0 being Neighbourhood of y0 such that

A17: ( N0 c= N & N0 c= N1 ) by RCOMP_1:17;

consider g being Real such that

A18: 0 < g and

A19: N0 = ].(y0 - g),(y0 + g).[ by RCOMP_1:def 6;

deffunc H

consider s1 being Real_Sequence such that

A20: for n being Nat holds s1 . n = H

now :: thesis: for n being Nat holds s1 . n <> 0

then A21:
s1 is non-zero
by SEQ_1:5;let n be Nat; :: thesis: s1 . n <> 0

g / (n + 2) <> 0 by A18, XREAL_1:139;

hence s1 . n <> 0 by A20; :: thesis: verum

end;g / (n + 2) <> 0 by A18, XREAL_1:139;

hence s1 . n <> 0 by A20; :: thesis: verum

( s1 is convergent & lim s1 = 0 ) by A20, SEQ_4:31;

then reconsider h = s1 as non-zero 0 -convergent 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

A24:
diff ((SVF1 (2,f,z)),y2) = p1 * 1
by A13, A15;
let n be Element of NAT ; :: thesis: ex y being Real st

( y in N & y in N1 & h . n = y - y0 )

take y0 + (g / (n + 2)) ; :: thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 )

0 + 1 < (n + 1) + 1 by XREAL_1:6;

then g / (n + 2) < g / 1 by A18, XREAL_1:76;

then A23: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6;

g / (n + 2) > 0 by A18, XREAL_1:139;

then y0 + (- g) < y0 + (g / (n + 2)) by A18, XREAL_1:6;

then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A23;

hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A17, A19, A20; :: thesis: verum

end;( y in N & y in N1 & h . n = y - y0 )

take y0 + (g / (n + 2)) ; :: thesis: ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 )

0 + 1 < (n + 1) + 1 by XREAL_1:6;

then g / (n + 2) < g / 1 by A18, XREAL_1:76;

then A23: y0 + (g / (n + 2)) < y0 + g by XREAL_1:6;

g / (n + 2) > 0 by A18, XREAL_1:139;

then y0 + (- g) < y0 + (g / (n + 2)) by A18, XREAL_1:6;

then y0 + (g / (n + 2)) in ].(y0 - g),(y0 + g).[ by A23;

hence ( y0 + (g / (n + 2)) in N & y0 + (g / (n + 2)) in N1 & h . n = (y0 + (g / (n + 2))) - y0 ) by A17, A19, A20; :: thesis: verum

A25: now :: thesis: for y being Real st y in N & y in N1 holds

((partdiff (f,z,2)) * (y - y0)) + (R . (y - y0)) = ((diff ((SVF1 (2,f,z)),y2)) * (y - y0)) + (R1 . (y - y0))

reconsider rd = (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) as Element of REAL by XREAL_0:def 1;((partdiff (f,z,2)) * (y - y0)) + (R . (y - y0)) = ((diff ((SVF1 (2,f,z)),y2)) * (y - y0)) + (R1 . (y - y0))

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

now :: thesis: for n being Nat holds rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n

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;
R1 is total
by FDIFF_1:def 2;

then dom R1 = REAL by PARTFUN1:def 2;

then A28: rng h c= dom R1 ;

let n be Nat; :: thesis: rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n

R is total by FDIFF_1:def 2;

then dom R = REAL by PARTFUN1:def 2;

then A29: rng h c= dom R ;

A30: n in NAT by ORDINAL1:def 12;

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

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:108

.= ((h ") (#) (R /* h)) . n by SEQ_1:8 ;

A33: h . n <> 0 by SEQ_1:5;

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:108

.= ((h ") (#) (R1 /* h)) . n by SEQ_1:8 ;

A35: ((diff ((SVF1 (2,f,z)),y2)) * (h . n)) / (h . n) = (diff ((SVF1 (2,f,z)),y2)) * ((h . n) / (h . n)) by XCMPLX_1:74

.= (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:74

.= (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:62;

then partdiff (f,z,2) = (diff ((SVF1 (2,f,z)),y2)) + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;

hence rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by RFUNCT_2:1; :: thesis: verum

end;then dom R1 = REAL by PARTFUN1:def 2;

then A28: rng h c= dom R1 ;

let n be Nat; :: thesis: rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n

R is total by FDIFF_1:def 2;

then dom R = REAL by PARTFUN1:def 2;

then A29: rng h c= dom R ;

A30: n in NAT by ORDINAL1:def 12;

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

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:108

.= ((h ") (#) (R /* h)) . n by SEQ_1:8 ;

A33: h . n <> 0 by SEQ_1:5;

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:108

.= ((h ") (#) (R1 /* h)) . n by SEQ_1:8 ;

A35: ((diff ((SVF1 (2,f,z)),y2)) * (h . n)) / (h . n) = (diff ((SVF1 (2,f,z)),y2)) * ((h . n) / (h . n)) by XCMPLX_1:74

.= (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:74

.= (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:62;

then partdiff (f,z,2) = (diff ((SVF1 (2,f,z)),y2)) + ((((h ") (#) (R1 /* h)) . n) - (((h ") (#) (R /* h)) . n)) by A32, A34;

hence rd = (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . n by RFUNCT_2:1; :: thesis: verum

then A36: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) by SEQ_4:25;

A37: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by FDIFF_1:def 2;

( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by FDIFF_1:def 2;

then (partdiff (f,z,2)) - (diff ((SVF1 (2,f,z)),y2)) = 0 - 0 by A36, A37, SEQ_2:12;

hence partdiff (f,z,2) = diff ((SVF1 (2,f,z)),y0) by A1, A10, FINSEQ_1:77; :: thesis: verum