let E, F, G be RealNormSpace; :: thesis: for u being PartFunc of E,F
for Z being Subset of E
for L being Lipschitzian LinearOperator of F,G st u is_differentiable_on Z holds
( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) )
let u be PartFunc of E,F; :: thesis: for Z being Subset of E
for L being Lipschitzian LinearOperator of F,G st u is_differentiable_on Z holds
( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) )
let Z be Subset of E; :: thesis: for L being Lipschitzian LinearOperator of F,G st u is_differentiable_on Z holds
( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) )
let L be Lipschitzian LinearOperator of F,G; :: thesis: ( u is_differentiable_on Z implies ( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) ) )
assume A1: u is_differentiable_on Z ; :: thesis: ( L * u is_differentiable_on Z & ( for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x) ) )
A2: u .: Z c= [#] F ;
A3: ( L is_differentiable_on [#] F & ( for x being Point of F holds (L `| ([#] F)) /. x = L ) ) by Th20;
hence L * u is_differentiable_on Z by A1, A2, Th19; :: thesis: for x being Point of E st x in Z holds
((L * u) `| Z) /. x = L * ((u `| Z) /. x)
let x be Point of E; :: thesis: ( x in Z implies ((L * u) `| Z) /. x = L * ((u `| Z) /. x) )
A4: modetrans (((L `| ([#] F)) /. (u /. x)),F,G) = (L `| ([#] F)) /. (u /. x) by LOPBAN_1:def 11
.= L by Th20 ;
assume x in Z ; :: thesis: ((L * u) `| Z) /. x = L * ((u `| Z) /. x)
then ((L * u) `| Z) /. x = ((L `| ([#] F)) /. (u /. x)) * ((u `| Z) /. x) by A1, A2, A3, Th19
.= L * ((u `| Z) /. x) by A4, LOPBAN_1:def 11 ;
hence ((L * u) `| Z) /. x = L * ((u `| Z) /. x) ; :: thesis: verum