theorem Th53: :: NDIFF_5:53

for G being RealNormSpace-Sequence
for S being RealNormSpace
for f being PartFunc of (product G),S
for X being Subset of (product G)
for x, y, z being Point of (product G)
for i being set
for p, q being Point of (G . (In (i,(dom G))))
for d, r being Real st i in dom G & X is open & x in X & ||.(y - x).|| < d & ||.(z - x).|| < d & X c= dom f & ( for x being Point of (product G) st x in X holds
f is_partial_differentiable_in x,i ) & ( for z being Point of (product G) st ||.(z - x).|| < d holds
z in X ) & ( for z being Point of (product G) st ||.(z - x).|| < d holds
||.((partdiff (f,z,i)) - (partdiff (f,x,i))).|| <= r ) & z = (reproj ((In (i,(dom G))),y)) . p & q = (proj (In (i,(dom G)))) . y holds
||.(((f /. z) - (f /. y)) - ((partdiff (f,x,i)) . (p - q))).|| <= ||.(p - q).|| * r