let S, E, F, G be RealNormSpace; :: thesis: for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for W being PartFunc of S,G
for w being PartFunc of S,[:E,F:]
for u being PartFunc of S,E
for v being PartFunc of S,F st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> holds
( W is_differentiable_on Z & W `| Z is_continuous_on Z )
let Z be Subset of S; :: thesis: for B being Lipschitzian BilinearOperator of E,F,G
for W being PartFunc of S,G
for w being PartFunc of S,[:E,F:]
for u being PartFunc of S,E
for v being PartFunc of S,F st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> holds
( W is_differentiable_on Z & W `| Z is_continuous_on Z )
let B be Lipschitzian BilinearOperator of E,F,G; :: thesis: for W being PartFunc of S,G
for w being PartFunc of S,[:E,F:]
for u being PartFunc of S,E
for v being PartFunc of S,F st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> holds
( W is_differentiable_on Z & W `| Z is_continuous_on Z )
let W be PartFunc of S,G; :: thesis: for w being PartFunc of S,[:E,F:]
for u being PartFunc of S,E
for v being PartFunc of S,F st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> holds
( W is_differentiable_on Z & W `| Z is_continuous_on Z )
let w be PartFunc of S,[:E,F:]; :: thesis: for u being PartFunc of S,E
for v being PartFunc of S,F st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> holds
( W is_differentiable_on Z & W `| Z is_continuous_on Z )
let u be PartFunc of S,E; :: thesis: for v being PartFunc of S,F st u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> holds
( W is_differentiable_on Z & W `| Z is_continuous_on Z )
let v be PartFunc of S,F; :: thesis: ( u is_differentiable_on Z & u `| Z is_continuous_on Z & v is_differentiable_on Z & v `| Z is_continuous_on Z & W = B * w & w = <:u,v:> implies ( W is_differentiable_on Z & W `| Z is_continuous_on Z ) )
assume that
A1: ( u is_differentiable_on Z & u `| Z is_continuous_on Z ) and
A2: ( v is_differentiable_on Z & v `| Z is_continuous_on Z ) and
A3: ( W = B * w & w = <:u,v:> ) ; :: thesis: ( W is_differentiable_on Z & W `| Z is_continuous_on Z )
A4: ( w is_differentiable_on Z & w `| Z is_continuous_on Z ) by A1, A2, A3, Th29;
A5: ( B is_differentiable_on [#] [:E,F:] & B `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] ) by NDIFF12:14;
w .: Z c= [#] [:E,F:] ;
hence ( W is_differentiable_on Z & W `| Z is_continuous_on Z ) by A3, A4, A5, Th23; :: thesis: verum