let S, T, W be RealNormSpace; :: thesis: 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; :: thesis: 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; :: thesis: 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)); :: thesis: ( 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: ( 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; :: thesis: 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; :: thesis: verum