defpred S₁[ Nat] means for S, E, F, G being RealNormSpace
for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on $1,Z & v is_differentiable_on $1,Z holds
W is_differentiable_on $1,Z;
A1: S₁[ 0 ]

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 u be PartFunc of S,E; :: thesis:
let v be PartFunc of S,F; :: thesis:
let w be PartFunc of S,[:E,F:]; :: thesis:
let W be PartFunc of S,G; :: thesis:
assume A2: ( W = B * w & w = <:u,v:> & u is_differentiable_on 0 ,Z & v is_differentiable_on 0 ,Z ) ; :: thesis:
dom B = [#] [:E,F:] by FUNCT_2:def 1;
then rng w c= dom B ;
then A3: dom W = dom w by A2, RELAT_1:27;
dom w = (dom u) /\ (dom v) by A2, FUNCT_3:def 7;
hence W is_differentiable_on 0 ,Z by A2, A3, XBOOLE_1:19; :: thesis:

end;

A4: for i being Nat st S₁[i] holds
S₁[i + 1]

proof

let i be Nat; :: thesis:
assume A5: S₁[i] ; :: thesis:
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 u be PartFunc of S,E; :: thesis:
let v be PartFunc of S,F; :: thesis:
let w be PartFunc of S,[:E,F:]; :: thesis:
let W be PartFunc of S,G; :: thesis:
assume A6: ( W = B * w & w = <:u,v:> & u is_differentiable_on i + 1,Z & v is_differentiable_on i + 1,Z ) ; :: thesis:
0 <= i by NAT_1:2;
then ( u is_differentiable_on 0 + 1,Z & v is_differentiable_on 0 + 1,Z ) by A6, NDIFF_6:17, XREAL_1:7;
then A7: ( u | Z is_differentiable_on Z & v | Z is_differentiable_on Z ) by NDIFF_6:15;
A8: u is_differentiable_on Z by A6, A7;
A9: v is_differentiable_on Z by A6, A7;
A10: ( W is_differentiable_on Z & ( 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))) ) ) by A6, A8, A9, Th35;
A11: u `| Z is_differentiable_on i,Z by A6, Th36;
A12: v `| Z is_differentiable_on i,Z by A6, Th36;
set V10 = the Point of E;
set V20 = the Point of F;
reconsider BP = B as Point of (R_NormSpace_of_BoundedBilinearOperators (E,F,G)) by LOPBAN_9:def 4;
defpred S₂[ object , object ] means ex V2 being Point of F st
( V2 = $1 & $2 = B * (reproj1 [ the Point of E,V2]) );
A13: for x being object st x in the carrier of F holds
ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) & S₂[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of F ; :: thesis:
then reconsider V2 = x as Point of F ;
A14: B * (reproj1 [ the Point of E,V2]) is Lipschitzian LinearOperator of E,G by NDIFF12:2;
take y = B * (reproj1 [ the Point of E,V2]); :: thesis:
thus ( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) & S₂[x,y] ) by A14, LOPBAN_1:def 9; :: thesis:

end;

consider B2 being Function of the carrier of F, the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) such that
A15: for x being object st x in the carrier of F holds
S₂[x,B2 . x] from FUNCT_2:sch 1(A13);
A16: for V2 being Point of F holds B2 . V2 = B * (reproj1 [ the Point of E,V2])

proof

let V2 be Point of F; :: thesis:
ex V being Point of F st
( V = V2 & B2 . V2 = B * (reproj1 [ the Point of E,V]) ) by A15;
hence B2 . V2 = B * (reproj1 [ the Point of E,V2]) ; :: thesis:

end;

defpred S₃[ object , object ] means ex V1 being Point of E st
( V1 = $1 & $2 = B * (reproj2 [V1, the Point of F]) );
A17: for x being object st x in the carrier of E holds
ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) & S₃[x,y] )

proof

let x be object ; :: thesis:
assume x in the carrier of E ; :: thesis:
then reconsider V1 = x as Point of E ;
A18: B * (reproj2 [V1, the Point of F]) is Lipschitzian LinearOperator of F,G by NDIFF12:2;
take y = B * (reproj2 [V1, the Point of F]); :: thesis:
thus ( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) & S₃[x,y] ) by A18, LOPBAN_1:def 9; :: thesis:

end;

consider B1 being Function of the carrier of E, the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) such that
A19: for x being object st x in the carrier of E holds
S₃[x,B1 . x] from FUNCT_2:sch 1(A17);
A20: for V1 being Point of E holds B1 . V1 = B * (reproj2 [V1, the Point of F])

proof

let V1 be Point of E; :: thesis:
ex V being Point of E st
( V1 = V & B1 . V1 = B * (reproj2 [V, the Point of F]) ) by A19;
hence B1 . V1 = B * (reproj2 [V1, the Point of F]) ; :: thesis:

end;

for x, y being Element of F holds B2 . (x + y) = (B2 . x) + (B2 . y)

proof

let x, y be Element of F; :: thesis:
A21: B2 . y = B * (reproj1 [ the Point of E,y]) by A16;
set f = B * (reproj1 [ the Point of E,x]);
set g = B * (reproj1 [ the Point of E,y]);
set h = B * (reproj1 [ the Point of E,(x + y)]);
for s being VECTOR of E holds (B2 . (x + y)) . s = ((B2 . x) . s) + ((B2 . y) . s)

proof

let s be VECTOR of E; :: thesis:
thus (B2 . (x + y)) . s = (B * (reproj1 [ the Point of E,(x + y)])) . s by A16
.= B . ((reproj1 [ the Point of E,(x + y)]) . s) by FUNCT_2:15
.= B . [s,([ the Point of E,(x + y)] `2)] by NDIFF_7:def 1
.= B . (s,(x + y)) by BINOP_1:def 1
.= (B . (s,x)) + (B . (s,y)) by LOPBAN_8:12
.= (B . [s,x]) + (B . (s,y)) by BINOP_1:def 1
.= (B . [s,([ the Point of E,x] `2)]) + (B . [s,y]) by BINOP_1:def 1
.= (B . ((reproj1 [ the Point of E,x]) . s)) + (B . [s,([ the Point of E,y] `2)]) by NDIFF_7:def 1
.= (B . ((reproj1 [ the Point of E,x]) . s)) + (B . ((reproj1 [ the Point of E,y]) . s)) by NDIFF_7:def 1
.= ((B * (reproj1 [ the Point of E,x])) . s) + (B . ((reproj1 [ the Point of E,y]) . s)) by FUNCT_2:15
.= ((B * (reproj1 [ the Point of E,x])) . s) + ((B * (reproj1 [ the Point of E,y])) . s) by FUNCT_2:15
.= ((B2 . x) . s) + ((B2 . y) . s) by A16, A21 ; :: thesis:

end;

hence B2 . (x + y) = (B2 . x) + (B2 . y) by LOPBAN_1:35; :: thesis:

end;

then A22: B2 is additive ;
for x being VECTOR of F
for a being Real holds B2 . (a * x) = a * (B2 . x)

proof

let x be VECTOR of F; :: thesis:
let a be Real; :: thesis:
set f = B * (reproj1 [ the Point of E,x]);
set g = B * (reproj1 [ the Point of E,(a * x)]);
for s being VECTOR of E holds (B2 . (a * x)) . s = a * ((B2 . x) . s)

proof

let s be VECTOR of E; :: thesis:
thus (B2 . (a * x)) . s = (B * (reproj1 [ the Point of E,(a * x)])) . s by A16
.= B . ((reproj1 [ the Point of E,(a * x)]) . s) by FUNCT_2:15
.= B . [s,([ the Point of E,(a * x)] `2)] by NDIFF_7:def 1
.= B . (s,(a * x)) by BINOP_1:def 1
.= a * (B . (s,x)) by LOPBAN_8:12
.= a * (B . [s,([ the Point of E,x] `2)]) by BINOP_1:def 1
.= a * (B . ((reproj1 [ the Point of E,x]) . s)) by NDIFF_7:def 1
.= a * ((B * (reproj1 [ the Point of E,x])) . s) by FUNCT_2:15
.= a * ((B2 . x) . s) by A16 ; :: thesis:

end;

hence B2 . (a * x) = a * (B2 . x) by LOPBAN_1:36; :: thesis:

end;

then reconsider B2 = B2 as LinearOperator of F,(R_NormSpace_of_BoundedLinearOperators (E,G)) by A22, LOPBAN_1:def 5;
for x, y being Element of E holds B1 . (x + y) = (B1 . x) + (B1 . y)

proof

let x, y be Element of E; :: thesis:
A23: B1 . y = B * (reproj2 [y, the Point of F]) by A20;
set f = B * (reproj2 [x, the Point of F]);
set g = B * (reproj2 [y, the Point of F]);
set h = B * (reproj2 [(x + y), the Point of F]);
for s being VECTOR of F holds (B1 . (x + y)) . s = ((B1 . x) . s) + ((B1 . y) . s)

proof

let s be VECTOR of F; :: thesis:
thus (B1 . (x + y)) . s = (B * (reproj2 [(x + y), the Point of F])) . s by A20
.= B . ((reproj2 [(x + y), the Point of F]) . s) by FUNCT_2:15
.= B . [([(x + y), the Point of F] `1),s] by NDIFF_7:def 2
.= B . ((x + y),s) by BINOP_1:def 1
.= (B . (x,s)) + (B . (y,s)) by LOPBAN_8:12
.= (B . [x,s]) + (B . (y,s)) by BINOP_1:def 1
.= (B . [([x, the Point of F] `1),s]) + (B . [y,s]) by BINOP_1:def 1
.= (B . ((reproj2 [x, the Point of F]) . s)) + (B . [([y, the Point of F] `1),s]) by NDIFF_7:def 2
.= (B . ((reproj2 [x, the Point of F]) . s)) + (B . ((reproj2 [y, the Point of F]) . s)) by NDIFF_7:def 2
.= ((B * (reproj2 [x, the Point of F])) . s) + (B . ((reproj2 [y, the Point of F]) . s)) by FUNCT_2:15
.= ((B * (reproj2 [x, the Point of F])) . s) + ((B * (reproj2 [y, the Point of F])) . s) by FUNCT_2:15
.= ((B1 . x) . s) + ((B1 . y) . s) by A20, A23 ; :: thesis:

end;

hence B1 . (x + y) = (B1 . x) + (B1 . y) by LOPBAN_1:35; :: thesis:

end;

then A24: B1 is additive ;
for x being VECTOR of E
for a being Real holds B1 . (a * x) = a * (B1 . x)

proof

let x be VECTOR of E; :: thesis:
let a be Real; :: thesis:
set f = B * (reproj2 [x, the Point of F]);
set g = B * (reproj2 [(a * x), the Point of F]);
for s being VECTOR of F holds (B1 . (a * x)) . s = a * ((B1 . x) . s)

proof

let s be VECTOR of F; :: thesis:
thus (B1 . (a * x)) . s = (B * (reproj2 [(a * x), the Point of F])) . s by A20
.= B . ((reproj2 [(a * x), the Point of F]) . s) by FUNCT_2:15
.= B . [([(a * x), the Point of F] `1),s] by NDIFF_7:def 2
.= B . ((a * x),s) by BINOP_1:def 1
.= a * (B . (x,s)) by LOPBAN_8:12
.= a * (B . [([x, the Point of F] `1),s]) by BINOP_1:def 1
.= a * (B . ((reproj2 [x, the Point of F]) . s)) by NDIFF_7:def 2
.= a * ((B * (reproj2 [x, the Point of F])) . s) by FUNCT_2:15
.= a * ((B1 . x) . s) by A20 ; :: thesis:

end;

hence B1 . (a * x) = a * (B1 . x) by LOPBAN_1:36; :: thesis:

end;

then reconsider B1 = B1 as LinearOperator of E,(R_NormSpace_of_BoundedLinearOperators (F,G)) by A24, LOPBAN_1:def 5;

now :: thesis:

let V2 be Point of F; :: thesis:
A25: B2 . V2 = B * (reproj1 [ the Point of E,V2]) by A16;
set L1 = B * (reproj1 [ the Point of E,V2]);
set z = [ the Point of E,V2];
consider BP0 being Point of (R_NormSpace_of_BoundedBilinearOperators (E,F,G)) such that
A26: ( B = BP0 & ( for x being VECTOR of E holds ||.((B * (reproj1 [ the Point of E,V2])) . x).|| <= (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * ||.x.|| ) & ( for y being VECTOR of F holds ||.((B * (reproj2 [ the Point of E,V2])) . y).|| <= (||.BP0.|| * ||.([ the Point of E,V2] `1).||) * ||.y.|| ) ) by NDIFF12:2;
A27: 0 <= ||.BP0.|| by NORMSP_1:4;
reconsider LL1 = B * (reproj1 [ the Point of E,V2]) as Lipschitzian LinearOperator of E,G by A25, LOPBAN_1:def 9;

A28: now :: thesis:

let t be VECTOR of E; :: thesis:
assume A29: ||.t.|| <= 1 ; :: thesis:
A30: ||.(LL1 . t).|| <= (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * ||.t.|| by A26;
0 <= ||.([ the Point of E,V2] `2).|| by NORMSP_1:4;
then 0 <= ||.BP0.|| * ||.([ the Point of E,V2] `2).|| by A27, XREAL_1:127;
then (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * ||.t.|| <= (||.BP0.|| * ||.([ the Point of E,V2] `2).||) * 1 by A29, XREAL_1:64;
hence ||.(LL1 . t).|| <= ||.BP0.|| * ||.([ the Point of E,V2] `2).|| by A30, XXREAL_0:2; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms LL1 ; :: thesis:
then ex t being VECTOR of E st
( r = ||.(LL1 . t).|| & ||.t.|| <= 1 ) ;
hence r <= ||.BP0.|| * ||.([ the Point of E,V2] `2).|| by A28; :: thesis:

end;

then upper_bound (PreNorms LL1) <= ||.BP0.|| * ||.([ the Point of E,V2] `2).|| by SEQ_4:45;
hence ||.(B2 . V2).|| <= ||.BP.|| * ||.V2.|| by A25, A26, LOPBAN_1:30; :: thesis:

end;

then reconsider B2 = B2 as Lipschitzian LinearOperator of F,(R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_1:def 8, NORMSP_1:4;

now :: thesis:

let V1 be Point of E; :: thesis:
A31: B1 . V1 = B * (reproj2 [V1, the Point of F]) by A20;
set L1 = B * (reproj2 [V1, the Point of F]);
set z = [V1, the Point of F];
consider BP0 being Point of (R_NormSpace_of_BoundedBilinearOperators (E,F,G)) such that
A32: ( B = BP0 & ( for x being VECTOR of E holds ||.((B * (reproj1 [V1, the Point of F])) . x).|| <= (||.BP0.|| * ||.([V1, the Point of F] `2).||) * ||.x.|| ) & ( for y being VECTOR of F holds ||.((B * (reproj2 [V1, the Point of F])) . y).|| <= (||.BP0.|| * ||.([V1, the Point of F] `1).||) * ||.y.|| ) ) by NDIFF12:2;
A33: 0 <= ||.BP0.|| by NORMSP_1:4;
reconsider LL1 = B * (reproj2 [V1, the Point of F]) as Lipschitzian LinearOperator of F,G by A31, LOPBAN_1:def 9;
A34: ( ( for s being Real st s in PreNorms LL1 holds
s <= ||.BP0.|| * ||.([V1, the Point of F] `1).|| ) implies upper_bound (PreNorms LL1) <= ||.BP0.|| * ||.([V1, the Point of F] `1).|| ) by SEQ_4:45;

A35: now :: thesis:

let t be VECTOR of F; :: thesis:
assume A36: ||.t.|| <= 1 ; :: thesis:
A37: ||.(LL1 . t).|| <= (||.BP0.|| * ||.([V1, the Point of F] `1).||) * ||.t.|| by A32;
0 <= ||.([V1, the Point of F] `1).|| by NORMSP_1:4;
then 0 <= ||.BP0.|| * ||.([V1, the Point of F] `1).|| by A33, XREAL_1:127;
then (||.BP0.|| * ||.([V1, the Point of F] `1).||) * ||.t.|| <= (||.BP0.|| * ||.([V1, the Point of F] `1).||) * 1 by A36, XREAL_1:64;
hence ||.(LL1 . t).|| <= ||.BP0.|| * ||.([V1, the Point of F] `1).|| by A37, XXREAL_0:2; :: thesis:

end;

now :: thesis:

let r be Real; :: thesis:
assume r in PreNorms LL1 ; :: thesis:
then ex t being VECTOR of F st
( r = ||.(LL1 . t).|| & ||.t.|| <= 1 ) ;
hence r <= ||.BP0.|| * ||.([V1, the Point of F] `1).|| by A35; :: thesis:

end;

hence ||.(B1 . V1).|| <= ||.BP.|| * ||.V1.|| by A31, A32, A34, LOPBAN_1:30; :: thesis:

end;

then reconsider B1 = B1 as Lipschitzian LinearOperator of E,(R_NormSpace_of_BoundedLinearOperators (F,G)) by LOPBAN_1:def 8, NORMSP_1:4;
A38: for x being Point of S st x in Z holds
for V being Point of E holds ((B2 * v) /. x) . V = B . (V,(v /. x))

proof

let x be Point of S; :: thesis:
assume A39: x in Z ; :: thesis:
v /. x in the carrier of F ;
then v /. x in dom B2 by FUNCT_2:def 1;
then A40: (B2 * v) /. x = B2 /. (v /. x) by A6, A39, PARTFUN2:4
.= B * (reproj1 [ the Point of E,(v /. x)]) by A16 ;
let V be Point of E; :: thesis:
A41: [ the Point of E,(v /. x)] `2 = v /. x ;
thus ((B2 * v) /. x) . V = B . ((reproj1 [ the Point of E,(v /. x)]) . V) by A40, FUNCT_2:15
.= B . [V,(v /. x)] by A41, NDIFF_7:def 1
.= B . (V,(v /. x)) by BINOP_1:def 1 ; :: thesis:

end;

A42: for x being Point of S st x in Z holds
for ds being Point of S holds B . ((((u `| Z) /. x) . ds),(v /. x)) = (((B2 * v) /. x) * ((u `| Z) /. x)) . ds

proof

let x be Point of S; :: thesis:
assume A43: x in Z ; :: thesis:
let ds be Point of S; :: thesis:
reconsider F1 = (B2 * v) /. x as Lipschitzian LinearOperator of E,G by LOPBAN_1:def 9;
reconsider F2 = (u `| Z) /. x as Lipschitzian LinearOperator of S,E by LOPBAN_1:def 9;
A44: modetrans (F2,S,E) = F2 by LOPBAN_1:def 11;
A45: dom F2 = the carrier of S by FUNCT_2:def 1;
thus (((B2 * v) /. x) * ((u `| Z) /. x)) . ds = (F1 * F2) . ds by A44, LOPBAN_1:def 11
.= ((B2 * v) /. x) . (((u `| Z) /. x) . ds) by A45, FUNCT_1:13
.= B . ((((u `| Z) /. x) . ds),(v /. x)) by A38, A43 ; :: thesis:

end;

A46: for x being Point of S st x in Z holds
for V being Point of F holds ((B1 * u) /. x) . V = B . ((u /. x),V)

proof

let x be Point of S; :: thesis:
assume A47: x in Z ; :: thesis:
u /. x in the carrier of E ;
then u /. x in dom B1 by FUNCT_2:def 1;
then A48: (B1 * u) /. x = B1 /. (u /. x) by A6, A47, PARTFUN2:4
.= B * (reproj2 [(u /. x), the Point of F]) by A20 ;
let V be Point of F; :: thesis:
A49: [(u /. x), the Point of F] `1 = u /. x ;
thus ((B1 * u) /. x) . V = B . ((reproj2 [(u /. x), the Point of F]) . V) by A48, FUNCT_2:15
.= B . [(u /. x),V] by A49, NDIFF_7:def 2
.= B . ((u /. x),V) by BINOP_1:def 1 ; :: thesis:

end;

A50: for x being Point of S st x in Z holds
for ds being Point of S holds B . ((u /. x),(((v `| Z) /. x) . ds)) = (((B1 * u) /. x) * ((v `| Z) /. x)) . ds

proof

let x be Point of S; :: thesis:
assume A51: x in Z ; :: thesis:
let ds be Point of S; :: thesis:
reconsider F1 = (B1 * u) /. x as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
reconsider F2 = (v `| Z) /. x as Lipschitzian LinearOperator of S,F by LOPBAN_1:def 9;
A52: modetrans (F2,S,F) = F2 by LOPBAN_1:def 11;
A53: dom F2 = the carrier of S by FUNCT_2:def 1;
thus (((B1 * u) /. x) * ((v `| Z) /. x)) . ds = (F1 * F2) . ds by A52, LOPBAN_1:def 11
.= ((B1 * u) /. x) . (((v `| Z) /. x) . ds) by A53, FUNCT_1:13
.= B . ((u /. x),(((v `| Z) /. x) . ds)) by A46, A51 ; :: thesis:

end;

A54: for x being Point of S st x in Z holds
for ds being Point of S holds ((W `| Z) /. x) . ds = ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds)

proof

let x be Point of S; :: thesis:
assume A55: x in Z ; :: thesis:
let ds be Point of S; :: thesis:
A56: B . ((((u `| Z) /. x) . ds),(v /. x)) = (((B2 * v) /. x) * ((u `| Z) /. x)) . ds by A42, A55;
thus ((W `| Z) /. x) . ds = (B . ((((u `| Z) /. x) . ds),(v /. x))) + (B . ((u /. x),(((v `| Z) /. x) . ds))) by A6, A8, A9, A55, Th35
.= ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds) by A50, A55, A56 ; :: thesis:

end;

A57: for x being Point of S st x in Z holds
(W `| Z) /. x = (((B2 * v) /. x) * ((u `| Z) /. x)) + (((B1 * u) /. x) * ((v `| Z) /. x))

proof

let x be Point of S; :: thesis:
assume x in Z ; :: thesis:
then for ds being Point of S holds ((W `| Z) /. x) . ds = ((((B2 * v) /. x) * ((u `| Z) /. x)) . ds) + ((((B1 * u) /. x) * ((v `| Z) /. x)) . ds) by A54;
hence (W `| Z) /. x = (((B2 * v) /. x) * ((u `| Z) /. x)) + (((B1 * u) /. x) * ((v `| Z) /. x)) by LOPBAN_1:35; :: thesis:

end;

proof

let x be Element of S; :: thesis:
assume A71: x in dom (W `| Z) ; :: thesis:
A72: dom (u `| Z) = Z by A8, NDIFF_1:def 9;
A73: (BX1 * w1) /. x = (BX1 * w1) . x by A63, A69, A71, PARTFUN1:def 6
.= BX1 . (w1 . x) by A60, A69, A71, FUNCT_1:13
.= BX1 . [((u `| Z) . x),((B2 * v) . x)] by A60, A69, A71, FUNCT_3:def 7
.= BX1 . [((u `| Z) /. x),((B2 * v) . x)] by A69, A71, A72, PARTFUN1:def 6
.= BX1 . [((u `| Z) /. x),((B2 * v) /. x)] by A58, A69, A71, PARTFUN1:def 6
.= BX1 . (((u `| Z) /. x),((B2 * v) /. x)) by BINOP_1:def 1
.= ((B2 * v) /. x) * ((u `| Z) /. x) by A59 ;
A74: dom (v `| Z) = Z by A9, NDIFF_1:def 9;
(BX2 * w2) /. x = (BX2 * w2) . x by A68, A69, A71, PARTFUN1:def 6
.= BX2 . (w2 . x) by A65, A69, A71, FUNCT_1:13
.= BX2 . [((v `| Z) . x),((B1 * u) . x)] by A65, A69, A71, FUNCT_3:def 7
.= BX2 . [((v `| Z) /. x),((B1 * u) . x)] by A69, A71, A74, PARTFUN1:def 6
.= BX2 . [((v `| Z) /. x),((B1 * u) /. x)] by A58, A69, A71, PARTFUN1:def 6
.= BX2 . (((v `| Z) /. x),((B1 * u) /. x)) by BINOP_1:def 1
.= ((B1 * u) /. x) * ((v `| Z) /. x) by A64 ;
hence (W `| Z) /. x = ((BX1 * w1) /. x) + ((BX2 * w2) /. x) by A57, A69, A71, A73; :: thesis:

end;

then A75: W `| Z = (BX1 * w1) + (BX2 * w2) by A69, A70, VFUNCT_1:def 1;
W `| Z is_differentiable_on i,Z

proof

per cases ;

suppose i = 0 ; :: thesis:

hence W `| Z is_differentiable_on i,Z by A10, NDIFF_1:def 9; :: thesis:

end;

suppose i <> 0 ; :: thesis:

hence W `| Z is_differentiable_on i,Z by A62, A67, A75, NDIFF_6:21, NAT_1:14; :: thesis:

end;

hence W is_differentiable_on i + 1,Z by A10, Th32; :: thesis:

end;

for i being Nat holds S₁[i] from NAT_1:sch 2(A1, A4);
hence for i being Nat
for S, E, F, G being RealNormSpace
for Z being Subset of S
for B being Lipschitzian BilinearOperator of E,F,G
for u being PartFunc of S,E
for v being PartFunc of S,F
for w being PartFunc of S,[:E,F:]
for W being PartFunc of S,G st W = B * w & w = <:u,v:> & u is_differentiable_on i,Z & v is_differentiable_on i,Z holds
W is_differentiable_on i,Z ; :: thesis: