let S, T, W be 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 )
let f be 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 )
let I be 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 )
let I0 be Point of (R_NormSpace_of_BoundedLinearOperators (S,T)); ( I0 = I implies 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 ) )
assume AS0:
I0 = I
; 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 )
let x be Point of S; ( f is_differentiable_in I . x implies ( f * I is_differentiable_in x & diff ((f * I),x) = (diff (f,(I . x))) * I0 ) )
assume AS4:
f is_differentiable_in I . x
; ( f * I is_differentiable_in x & diff ((f * I),x) = (diff (f,(I . x))) * I0 )
X1:
( I is_differentiable_in x & diff (I,x) = I )
by LM090;
thus
f * I is_differentiable_in x
by X1, AS4, NDIFF_2:13; diff ((f * I),x) = (diff (f,(I . x))) * I0
thus
diff ((f * I),x) = (diff (f,(I . x))) * I0
by AS0, AS4, X1, NDIFF_2:13; verum