let E, F, G be RealNormSpace; :: thesis: for f being Lipschitzian BilinearOperator of E,F,G holds
( f `| ([#] [:E,F:]) is Lipschitzian LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) & f `| ([#] [:E,F:]) is_differentiable_on [#] [:E,F:] & f `| ([#] [:E,F:]) is_continuous_on the carrier of [:E,F:] & ( for z being Point of [:E,F:] holds diff ((f `| ([#] [:E,F:])),z) = f `| ([#] [:E,F:]) ) )
let f be Lipschitzian BilinearOperator of E,F,G; :: thesis: ( f `| ([#] [:E,F:]) is Lipschitzian LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) & f `| ([#] [:E,F:]) is_differentiable_on [#] [:E,F:] & f `| ([#] [:E,F:]) is_continuous_on the carrier of [:E,F:] & ( for z being Point of [:E,F:] holds diff ((f `| ([#] [:E,F:])),z) = f `| ([#] [:E,F:]) ) )
set Z = [#] [:E,F:];
set B = R_NormSpace_of_BoundedLinearOperators ([:E,F:],G);
A1: ( f is_differentiable_on [#] [:E,F:] & f `| ([#] [:E,F:]) is_continuous_on [#] [:E,F:] ) by Th14;
set L = f `| ([#] [:E,F:]);
A2: rng (f `| ([#] [:E,F:])) c= the carrier of (R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) ;
dom (f `| ([#] [:E,F:])) = [#] [:E,F:] by A1, NDIFF_1:def 9;
then reconsider L = f `| ([#] [:E,F:]) as Function of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) by A2, FUNCT_2:2;
for x, y being Element of [:E,F:] holds L . (x + y) = (L . x) + (L . y)

proof

let x, y be Element of [:E,F:]; :: thesis: L . (x + y) = (L . x) + (L . y)
thus L . (x + y) = L /. (x + y)
.= diff (f,(x + y)) by A1, NDIFF_1:def 9
.= (diff (f,x)) + (diff (f,y)) by Th13
.= (L /. x) + (diff (f,y)) by A1, NDIFF_1:def 9
.= (L /. x) + (L /. y) by A1, NDIFF_1:def 9
.= (L . x) + (L . y) ; :: thesis: verum

end;

then A3: L is additive ;
for x being VECTOR of [:E,F:]
for a being Real holds L . (a * x) = a * (L . x)

proof

let x be VECTOR of [:E,F:]; :: thesis: for a being Real holds L . (a * x) = a * (L . x)
let a be Real; :: thesis: L . (a * x) = a * (L . x)
thus L . (a * x) = L /. (a * x)
.= diff (f,(a * x)) by A1, NDIFF_1:def 9
.= a * (diff (f,x)) by Th13
.= a * (L /. x) by A1, NDIFF_1:def 9
.= a * (L . x) ; :: thesis: verum

end;

then reconsider L = L as LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) by A3, LOPBAN_1:def 5;
consider K being Real such that
A4: ( 0 <= K & ( for z being Point of [:E,F:] holds
( f is_differentiable_in z & ( for dx being Point of E
for dy being Point of F holds (diff (f,z)) . (dx,dy) = (f . (dx,(z `2))) + (f . ((z `1),dy)) ) & ||.(diff (f,z)).|| <= K * ||.z.|| ) ) ) by Th11;
for y being VECTOR of [:E,F:] holds ||.(L . y).|| <= K * ||.y.||

proof

let y be VECTOR of [:E,F:]; :: thesis: ||.(L . y).|| <= K * ||.y.||
L . y = L /. y
.= diff (f,y) by A1, NDIFF_1:def 9 ;
hence ||.(L . y).|| <= K * ||.y.|| by A4; :: thesis: verum

end;

then reconsider L = L as Lipschitzian LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) by A4, LOPBAN_1:def 8;
for z being Point of [:E,F:] holds diff (L,z) = L by NDIFF_7:26;
hence ( f `| ([#] [:E,F:]) is Lipschitzian LinearOperator of [:E,F:],(R_NormSpace_of_BoundedLinearOperators ([:E,F:],G)) & f `| ([#] [:E,F:]) is_differentiable_on [#] [:E,F:] & f `| ([#] [:E,F:]) is_continuous_on the carrier of [:E,F:] & ( for z being Point of [:E,F:] holds diff ((f `| ([#] [:E,F:])),z) = f `| ([#] [:E,F:]) ) ) by A1, NDIFF_1:def 9, NDIFF_7:26; :: thesis: verum