theorem :: NDIFF13:17

for E, F, G being RealNormSpace
for u being PartFunc of E,F
for L being Lipschitzian LinearOperator of F,G
for x being Point of E st u is_differentiable_in x holds
( L * u is_differentiable_in x & diff ((L * u),x) = L * (diff (u,x)) )