let f be PartFunc of (REAL 3),REAL; for u0 being Element of REAL 3
for N being Neighbourhood of (proj (3,3)) . u0 st f is_hpartial_differentiable`33_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,3)),u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) )
let u0 be Element of REAL 3; for N being Neighbourhood of (proj (3,3)) . u0 st f is_hpartial_differentiable`33_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,3)),u0)) holds
for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) )
let N be Neighbourhood of (proj (3,3)) . u0; ( f is_hpartial_differentiable`33_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,3)),u0)) implies for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) ) )
assume A1:
( f is_hpartial_differentiable`33_in u0 & N c= dom (SVF1 (3,(pdiff1 (f,3)),u0)) )
; for h being non-zero 0 -convergent Real_Sequence
for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) )
let h be non-zero 0 -convergent Real_Sequence; for c being constant Real_Sequence st rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N holds
( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) )
let c be constant Real_Sequence; ( rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N implies ( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) ) )
assume A2:
( rng c = {((proj (3,3)) . u0)} & rng (h + c) c= N )
; ( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) )
A3:
pdiff1 (f,3) is_partial_differentiable_in u0,3
by A1, Th27;
consider x0, y0, z0 being Element of REAL such that
A4:
u0 = <*x0,y0,z0*>
by FINSEQ_2:103;
partdiff ((pdiff1 (f,3)),u0,3) =
diff ((SVF1 (3,(pdiff1 (f,3)),u0)),z0)
by A4, PDIFF_4:21
.=
hpartdiff33 (f,u0)
by A1, A4, Th18
;
hence
( (h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c)) is convergent & hpartdiff33 (f,u0) = lim ((h ") (#) (((SVF1 (3,(pdiff1 (f,3)),u0)) /* (h + c)) - ((SVF1 (3,(pdiff1 (f,3)),u0)) /* c))) )
by A1, A2, A3, PDIFF_4:27; verum