let E, F, G be RealNormSpace; :: thesis: ex B being Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (E,G)) st
for u being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds B . (u,v) = v * u
set EF = the carrier of (R_NormSpace_of_BoundedLinearOperators (E,F));
set FG = the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G));
set EG = the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G));
defpred S₁[ Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (E,F)), Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)), object ] means $3 = $2 * $1;
A1: for x being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) ex z being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) st S₁[x,y,z] ;
consider L being Function of [: the carrier of (R_NormSpace_of_BoundedLinearOperators (E,F)), the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)):], the carrier of (R_NormSpace_of_BoundedLinearOperators (E,G)) such that
A2: for x being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y being Element of the carrier of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds S₁[x,y,L . (x,y)] from BINOP_1:sch 3(A1);
set LEF = R_NormSpace_of_BoundedLinearOperators (E,F);
set LFG = R_NormSpace_of_BoundedLinearOperators (F,G);
set LEG = R_NormSpace_of_BoundedLinearOperators (E,G);
A3: for x1, x2 being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

proof

let x1, x2 be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
let y be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
thus L . ((x1 + x2),y) = y * (x1 + x2) by A2
.= (y * x1) + (y * x2) by LOPBAN13:19
.= (L . (x1,y)) + (y * x2) by A2
.= (L . (x1,y)) + (L . (x2,y)) by A2 ; :: thesis: verum

end;

A4: for x being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for a being Real holds L . ((a * x),y) = a * (L . (x,y))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let y be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let a be Real; :: thesis: L . ((a * x),y) = a * (L . (x,y))
thus L . ((a * x),y) = y * (a * x) by A2
.= (a * y) * x by LOPBAN13:28
.= a * (y * x) by LOPBAN13:28
.= a * (L . (x,y)) by A2 ; :: thesis: verum

end;

A5: for x being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y1, y2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for y1, y2 being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
let y1, y2 be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
thus L . (x,(y1 + y2)) = (y1 + y2) * x by A2
.= (y1 * x) + (y2 * x) by LOPBAN13:20
.= (L . (x,y1)) + (y2 * x) by A2
.= (L . (x,y1)) + (L . (x,y2)) by A2 ; :: thesis: verum

end;

A6: for x being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (F,G))
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let y be Point of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let a be Real; :: thesis: L . (x,(a * y)) = a * (L . (x,y))
thus L . (x,(a * y)) = (a * y) * x by A2
.= a * (y * x) by LOPBAN13:28
.= a * (L . (x,y)) by A2 ; :: thesis: verum

end;

reconsider L = L as BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (E,G)) by A3, A4, A5, A6, LOPBAN_8:12;
set K = 1;
for x being VECTOR of (R_NormSpace_of_BoundedLinearOperators (E,F))
for y being VECTOR of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.||

proof

let x be VECTOR of (R_NormSpace_of_BoundedLinearOperators (E,F)); :: thesis: for y being VECTOR of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.||
let y be VECTOR of (R_NormSpace_of_BoundedLinearOperators (F,G)); :: thesis: ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.||
reconsider x1 = x as Lipschitzian LinearOperator of E,F by LOPBAN_1:def 9;
reconsider y1 = y as Lipschitzian LinearOperator of F,G by LOPBAN_1:def 9;
A7: modetrans (x,E,F) = x1 by LOPBAN_1:def 11;
(BoundedLinearOperatorsNorm (E,G)) . (y1 * x1) <= ((BoundedLinearOperatorsNorm (F,G)) . y1) * ((BoundedLinearOperatorsNorm (E,F)) . x1) by LOPBAN_2:2;
then ||.(y * x).|| <= ||.y.|| * ||.x.|| by A7, LOPBAN_1:def 11;
hence ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.|| by A2; :: thesis: verum

end;

then reconsider L = L as Lipschitzian BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (E,F)),(R_NormSpace_of_BoundedLinearOperators (F,G)),(R_NormSpace_of_BoundedLinearOperators (E,G)) by LOPBAN_9:def 3;
take L ; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds L . (u,v) = v * u
thus for u being Point of (R_NormSpace_of_BoundedLinearOperators (E,F))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (F,G)) holds L . (u,v) = v * u by A2; :: thesis: verum