theorem Th16: :: NDIFF11:16

for X, Y being RealNormSpace
for x being Point of X
for f being Lipschitzian LinearOperator of X,Y holds
( f is_differentiable_in x & f = diff (f,x) )