theorem Th51: :: NDIFF_5:51

for G being RealNormSpace-Sequence
for F being RealNormSpace
for f being PartFunc of (product G),F
for x being Point of (product G)
for i being set
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators ((G . (In (i,(dom G)))),F))
for p, q being Point of (G . (In (i,(dom G)))) st i in dom G & ( for h being Point of (G . (In (i,(dom G)))) st h in ].p,q.[ holds
||.((partdiff (f,((reproj ((In (i,(dom G))),x)) . h),i)) - L).|| <= M ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds
(reproj ((In (i,(dom G))),x)) . h in dom f ) & ( for h being Point of (G . (In (i,(dom G)))) st h in [.p,q.] holds
f is_partial_differentiable_in (reproj ((In (i,(dom G))),x)) . h,i ) holds
||.(((f /. ((reproj ((In (i,(dom G))),x)) . q)) - (f /. ((reproj ((In (i,(dom G))),x)) . p))) - (L . (q - p))).|| <= M * ||.(q - p).||