let E, F, G be RealNormSpace; :: thesis: for Z being Subset of E
for u being PartFunc of E,F
for L being Lipschitzian LinearOperator of F,G
for i being Nat st u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) is_continuous_on Z )
let Z be Subset of E; :: thesis: for u being PartFunc of E,F
for L being Lipschitzian LinearOperator of F,G
for i being Nat st u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) is_continuous_on Z )
let u be PartFunc of E,F; :: thesis: for L being Lipschitzian LinearOperator of F,G
for i being Nat st u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) is_continuous_on Z )
let L be Lipschitzian LinearOperator of F,G; :: thesis: for i being Nat st u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z holds
( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) is_continuous_on Z )
let i be Nat; :: thesis: ( u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z implies ( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) is_continuous_on Z ) )
assume A1: ( u is_differentiable_on i,Z & diff (u,i,Z) is_continuous_on Z ) ; :: thesis: ( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) is_continuous_on Z )
hence L * u is_differentiable_on i,Z by Th25; :: thesis: diff ((L * u),i,Z) is_continuous_on Z
A2: ( L * u is_differentiable_on i,Z & diff ((L * u),i,Z) = (LTRN (i,L,E)) * (diff (u,i,Z)) ) by A1, Th25;
A3: (diff (u,i,Z)) .: Z c= [#] (diff_SP (i,E,F)) ;
LTRN (i,L,E) is_continuous_on [#] (diff_SP (i,E,F)) by LOPBAN_5:4;
hence diff ((L * u),i,Z) is_continuous_on Z by A1, A2, A3, Th16; :: thesis: verum