let S, E, F, G be RealNormSpace; :: 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
for x being Point of S st u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> holds
( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
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
for x being Point of S st u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> holds
( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
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
for x being Point of S st u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> holds
( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
let w be PartFunc of S,[:E,F:]; :: thesis: for u being PartFunc of S,E
for v being PartFunc of S,F
for x being Point of S st u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> holds
( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
let u be PartFunc of S,E; :: thesis: for v being PartFunc of S,F
for x being Point of S st u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> holds
( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
let v be PartFunc of S,F; :: thesis: for x being Point of S st u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> holds
( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
let x be Point of S; :: thesis: ( u is_differentiable_in x & v is_differentiable_in x & x in dom w & W = B * w & w = <:u,v:> implies ( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) ) )
assume that
A1: u is_differentiable_in x and
A2: v is_differentiable_in x and
A3: ( x in dom w & W = B * w & w = <:u,v:> ) ; :: thesis: ( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) )
dom w = (dom u) /\ (dom v) by A3, FUNCT_3:def 7;
then A4: ( x in dom u & x in dom v ) by A3, XBOOLE_0:def 4;
A5: w /. x = w . x by A3, PARTFUN1:def 6
.= [(u . x),(v . x)] by A3, FUNCT_3:def 7
.= [(u /. x),(v . x)] by A4, PARTFUN1:def 6
.= [(u /. x),(v /. x)] by A4, PARTFUN1:def 6 ;
A6: ( w is_differentiable_in x & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for dx being Point of S holds (diff (w,x)) . dx = [((diff (u,x)) . dx),((diff (v,x)) . dx)] ) ) by A1, A2, A3, Th27;
consider K being Real such that
A7: ( 0 <= K & ( for z being Point of [:E,F:] holds
( B is_differentiable_in z & ( for dx being Point of E
for dy being Point of F holds (diff (B,z)) . (dx,dy) = (B . (dx,(z `2))) + (B . ((z `1),dy)) ) & ||.(diff (B,z)).|| <= K * ||.z.|| ) ) ) by NDIFF12:11;
A8: B is_differentiable_in w /. x by A7;
reconsider wx = diff (w,x) as Lipschitzian LinearOperator of S,[:E,F:] by LOPBAN_1:def 9;
A9: dom wx = the carrier of S by FUNCT_2:def 1;
reconsider Bwx = diff (B,(w /. x)) as Lipschitzian LinearOperator of [:E,F:],G by LOPBAN_1:def 9;
A10: modetrans ((diff (w,x)),S,[:E,F:]) = wx by LOPBAN_1:def 11;

now :: thesis: for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds)))

let ds be Point of S; :: thesis: (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds)))
thus (diff (W,x)) . ds = ((diff (B,(w /. x))) * (diff (w,x))) . ds by A3, A6, A8, NDIFF_2:13
.= (Bwx * wx) . ds by A10, LOPBAN_1:def 11
.= (diff (B,(w /. x))) . ((diff (w,x)) . ds) by A9, FUNCT_1:13
.= (diff (B,(w /. x))) . [((diff (u,x)) . ds),((diff (v,x)) . ds)] by A1, A2, A3, Th27
.= (diff (B,(w /. x))) . (((diff (u,x)) . ds),((diff (v,x)) . ds)) by BINOP_1:def 1
.= (B . (((diff (u,x)) . ds),((w /. x) `2))) + (B . (((w /. x) `1),((diff (v,x)) . ds))) by A7
.= (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) by A5 ; :: thesis: verum

end;

hence ( W is_differentiable_in x & w is_differentiable_in x & diff (W,x) = (diff (B,[(u /. x),(v /. x)])) * (diff (w,x)) & diff (w,x) = <:(diff (u,x)),(diff (v,x)):> & ( for ds being Point of S holds (diff (W,x)) . ds = (B . (((diff (u,x)) . ds),(v /. x))) + (B . ((u /. x),((diff (v,x)) . ds))) ) ) by A3, A5, A6, A8, NDIFF_2:13; :: thesis: verum