let f be PartFunc of (REAL 3),REAL ; :: thesis: for u0 being Element of REAL 3
for N being Neighbourhood of (proj 2,3) . u0 st f is_hpartial_differentiable`32_in u0 & N c= dom (SVF1 2,(pdiff1 f,3),u0) holds
for h being convergent_to_0 Real_Sequence
for c being V20() Real_Sequence st rng c = {((proj 2,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) )
let u0 be Element of REAL 3; :: thesis: for N being Neighbourhood of (proj 2,3) . u0 st f is_hpartial_differentiable`32_in u0 & N c= dom (SVF1 2,(pdiff1 f,3),u0) holds
for h being convergent_to_0 Real_Sequence
for c being V20() Real_Sequence st rng c = {((proj 2,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) )
let N be Neighbourhood of (proj 2,3) . u0; :: thesis: ( f is_hpartial_differentiable`32_in u0 & N c= dom (SVF1 2,(pdiff1 f,3),u0) implies for h being convergent_to_0 Real_Sequence
for c being V20() Real_Sequence st rng c = {((proj 2,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) ) )
assume A1: ( f is_hpartial_differentiable`32_in u0 & N c= dom (SVF1 2,(pdiff1 f,3),u0) ) ; :: thesis: for h being convergent_to_0 Real_Sequence
for c being V20() Real_Sequence st rng c = {((proj 2,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) )
let h be convergent_to_0 Real_Sequence; :: thesis: for c being V20() Real_Sequence st rng c = {((proj 2,3) . u0)} & rng (h + c) c= N holds
( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) )
let c be V20() Real_Sequence; :: thesis: ( rng c = {((proj 2,3) . u0)} & rng (h + c) c= N implies ( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) ) )
assume A2: ( rng c = {((proj 2,3) . u0)} & rng (h + c) c= N ) ; :: thesis: ( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) )
A3: pdiff1 f,3 is_partial_differentiable_in u0,2 by A1, Th12ForSecondOrder;
consider x0, y0, z0 being Real such that
A4: u0 = <*x0,y0,z0*> by FINSEQ_2:123;
partdiff (pdiff1 f,3),u0,2 = diff (SVF1 2,(pdiff1 f,3),u0),y0 by A4, PDIFF_4:20
.= hpartdiff32 f,u0 by A1, A4, Th8ForSecondOrder ;
hence ( (h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c)) is convergent & hpartdiff32 f,u0 = lim ((h " ) (#) (((SVF1 2,(pdiff1 f,3),u0) /* (h + c)) - ((SVF1 2,(pdiff1 f,3),u0) /* c))) ) by A1, A2, A3, PDIFF_4:26; :: thesis: verum