theorem LM120: :: NDIFF_7:27

for S, T, W being RealNormSpace
for f being PartFunc of T,W
for I being Lipschitzian LinearOperator of S,T
for I0 being Point of (R_NormSpace_of_BoundedLinearOperators (S,T)) st I0 = I holds
for x being Point of S st f is_differentiable_in I . x holds
( f * I is_differentiable_in x & diff ((f * I),x) = (diff (f,(I . x))) * I0 )