theorem Th20: :: NDIFF13:19

for F, G being RealNormSpace
for L being Lipschitzian LinearOperator of F,G holds
( L is_differentiable_on [#] F & L `| ([#] F) is_continuous_on [#] F & ( for x being Point of F holds (L `| ([#] F)) /. x = L ) )