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 st u is_differentiable_on Z & u `| Z is_continuous_on Z holds
( L * u is_differentiable_on Z & (L * u) `| 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 st u is_differentiable_on Z & u `| Z is_continuous_on Z holds
( L * u is_differentiable_on Z & (L * u) `| Z is_continuous_on Z )
let u be PartFunc of E,F; :: thesis: for L being Lipschitzian LinearOperator of F,G st u is_differentiable_on Z & u `| Z is_continuous_on Z holds
( L * u is_differentiable_on Z & (L * u) `| Z is_continuous_on Z )
let L be Lipschitzian LinearOperator of F,G; :: thesis: ( u is_differentiable_on Z & u `| Z is_continuous_on Z implies ( L * u is_differentiable_on Z & (L * u) `| Z is_continuous_on Z ) )
assume A1: ( u is_differentiable_on Z & u `| Z is_continuous_on Z ) ; :: thesis: ( L * u is_differentiable_on Z & (L * u) `| Z is_continuous_on Z )
A2: u .: Z c= [#] F ;
( L is_differentiable_on [#] F & L `| ([#] F) is_continuous_on [#] F ) by Th20;
hence ( L * u is_differentiable_on Z & (L * u) `| Z is_continuous_on Z ) by A1, A2, Th23; :: thesis: verum