let f be PartFunc of (REAL 2),REAL; :: thesis: for z0 being Element of REAL 2
for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let z0 be Element of REAL 2; :: thesis: for N being Neighbourhood of (proj (2,2)) . z0 st f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let N be Neighbourhood of (proj (2,2)) . z0; :: thesis: ( f is_hpartial_differentiable`22_in z0 & N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) )
assume that
A1: f is_hpartial_differentiable`22_in z0 and
A2: N c= dom (SVF1 (2,(pdiff1 (f,2)),z0)) ; :: thesis: for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; :: thesis: for c being constant Real_Sequence st rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
let c be constant Real_Sequence; :: thesis: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) )
assume A3: ( rng c = {((proj (2,2)) . z0)} & rng (h + c) c= N ) ; :: thesis: ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) )
consider x0, y0 being Element of REAL such that
A4: z0 = <*x0,y0*> by FINSEQ_2:100;
A5: pdiff1 (f,2) is_partial_differentiable_in z0,2 by A1, Th12;
then partdiff ((pdiff1 (f,2)),z0,2) = diff ((SVF1 (2,(pdiff1 (f,2)),z0)),y0) by A4, PDIFF_2:14
.= hpartdiff22 (f,z0) by A1, A4, Th8 ;
hence ( (h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c)) is convergent & hpartdiff22 (f,z0) = lim ((h ") (#) (((SVF1 (2,(pdiff1 (f,2)),z0)) /* (h + c)) - ((SVF1 (2,(pdiff1 (f,2)),z0)) /* c))) ) by A2, A3, A5, PDIFF_2:18; :: thesis: verum