let f be PartFunc of (REAL 2),REAL ; :: thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj 1,2) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 1,(pdiff1 f,2),z0) holds
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) )
let z0 be Element of REAL 2; :: thesis: for N being Neighbourhood of (proj 1,2) . z0 st f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 1,(pdiff1 f,2),z0) holds
for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) )
let N be Neighbourhood of (proj 1,2) . z0; :: thesis: ( f is_hpartial_differentiable`21_in z0 & N c= dom (SVF1 1,(pdiff1 f,2),z0) implies for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) ) )
assume that
A1: f is_hpartial_differentiable`21_in z0 and
A2: N c= dom (SVF1 1,(pdiff1 f,2),z0) ; :: thesis: for h being convergent_to_0 Real_Sequence
for c being V8() Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) )
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V8() Real_Sequence st rng c = {((proj 1,2) . z0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) )
let c be V8() Real_Sequence; :: thesis: ( rng c = {((proj 1,2) . z0)} & rng (h + c) c= N implies ( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) ) )
assume A3: ( rng c = {((proj 1,2) . z0)} & rng (h + c) c= N ) ; :: thesis: ( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) )
z0 is Tuple of 2, REAL by FINSEQ_2:151;
then consider x0, y0 being Real such that
A4: z0 = <*x0,y0*> by FINSEQ_2:120;
A5: pdiff1 f,2 is_partial_differentiable_in z0,1 by A1, Th11;
then partdiff (pdiff1 f,2),z0,1 = diff (SVF1 1,(pdiff1 f,2),z0),x0 by A4, PDIFF_2:13
.= hpartdiff21 f,z0 by A1, A4, Th7 ;
hence ( (h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c)) is convergent & hpartdiff21 f,z0 = lim ((h " ) (#) (((SVF1 1,(pdiff1 f,2),z0) /* (h + c)) - ((SVF1 1,(pdiff1 f,2),z0) /* c))) ) by A2, A3, A5, PDIFF_2:17; :: thesis: verum