let S, E, F, G be RealNormSpace; :: thesis:
let Z be Subset of S; :: thesis:
let B be Lipschitzian BilinearOperator of E,F,G; :: thesis:
let W be PartFunc of S,G; :: thesis:
let w be PartFunc of S,[:E,F:]; :: thesis:
let u be PartFunc of S,E; :: thesis:
let v be PartFunc of S,F; :: thesis:
assume that
A1: u is_differentiable_on Z and
A2: v is_differentiable_on Z and
A3: ( W = B * w & w = <:u,v:> ) ; :: thesis:
A4: ( w is_differentiable_on Z & ( for x being Point of S st x in Z holds
(w `| Z) /. x = <:((u `| Z) /. x),((v `| Z) /. x):> ) & ( for x being Point of S st x in Z holds
for dx being Point of S holds ((w `| Z) /. x) . dx = [(((u `| Z) /. x) . dx),(((v `| Z) /. x) . dx)] ) ) by A1, A2, A3, Th28;
A5: B is_differentiable_on [#] [:E,F:] by NDIFF12:14;
w .: Z c= [#] [:E,F:] ;
hence A6: W is_differentiable_on Z by A3, A4, A5, Th19; :: thesis:
A7: Z is open by NDIFF_1:32, A1;
thus for x being Point of S st x in Z holds
for ds being Point of S holds ((W `| Z) /. x) . ds = (B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds))) :: thesis:

proof

let x be Point of S; :: thesis:
assume A8: x in Z ; :: thesis:
then A9: u is_differentiable_in x by A1, A7, NDIFF_1:31;
A10: v is_differentiable_in x by A2, A7, A8, NDIFF_1:31;
let ds be Point of S; :: thesis:
A11: (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) by A3, A4, A8, A9, A10, Th34;
A12: (W `| Z) /. x = diff (W,x) by A6, A8, NDIFF_1:def 9;
(u `| Z) /. x = diff (u,x) by A1, A8, NDIFF_1:def 9;
hence ((W `| Z) /. x) . ds = (B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds))) by A2, A8, A11, A12, NDIFF_1:def 9; :: thesis:

end;