for S, T being RealNormSpace
for f being PartFunc of S,T
for p, q being Point of S
for M being Real 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)).|| <= M ) holds
||.((f /. q) - (f /. p)).|| <= M * ||.(q - p).||