theorem LM090: :: NDIFF_7:26

for S, T being RealNormSpace
for L being Lipschitzian LinearOperator of S,T
for x0 being Point of S holds
( L is_differentiable_in x0 & diff (L,x0) = L )