theorem Th20: :: NDIFF_5:20

for S, T being RealNormSpace
for f being PartFunc of S,T
for p, q being Point of S
for M being Real
for L being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st [.p,q.] c= dom f & ( for x being Point of S st x in [.p,q.] holds
f is_continuous_in x ) & ( for x being Point of S st x in ].p,q.[ holds
f is_differentiable_in x ) & ( for x being Point of S st x in ].p,q.[ holds
||.((diff (f,x)) - L).|| <= M ) holds
||.(((f /. q) - (f /. p)) - (L . (q - p))).|| <= M * ||.(q - p).||