theorem Th519: :: ORDEQ_02:12

for Y being RealNormSpace
for g being PartFunc of REAL, the carrier of Y
for a, b, M being Real st a <= b & [.a,b.] c= dom g & ( for x being Real st x in [.a,b.] holds
g is_continuous_in x ) & ( for x being Real st x in ].a,b.[ holds
g is_differentiable_in x ) & ( for x being Real st x in ].a,b.[ holds
||.(diff (g,x)).|| <= M ) holds
||.((g /. b) - (g /. a)).|| <= M * |.(b - a).|