let E, F, G be RealNormSpace; :: thesis: 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)) )
let u be PartFunc of E,F; :: thesis: 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)) )
let L be Lipschitzian LinearOperator of F,G; :: thesis: 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)) )
let x be Point of E; :: thesis: ( u is_differentiable_in x implies ( L * u is_differentiable_in x & diff ((L * u),x) = L * (diff (u,x)) ) )
assume A1: u is_differentiable_in x ; :: thesis: ( L * u is_differentiable_in x & diff ((L * u),x) = L * (diff (u,x)) )
A2: ( L is_differentiable_in u /. x & diff (L,(u /. x)) = L ) by NDIFF_7:26;
then A3: ( L * u is_differentiable_in x & diff ((L * u),x) = (diff (L,(u /. x))) * (diff (u,x)) ) by A1, NDIFF_2:13;
modetrans ((diff (u,x)),E,F) = diff (u,x) by LOPBAN_1:def 11;
hence ( L * u is_differentiable_in x & diff ((L * u),x) = L * (diff (u,x)) ) by A2, A3, LOPBAN_1:def 11; :: thesis: verum