let X, Y, Z be RealNormSpace; :: thesis: ex I being BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) st
( I is_continuous_on the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds I . (u,v) = v * u ) )
set E = R_NormSpace_of_BoundedLinearOperators (X,Y);
set F = R_NormSpace_of_BoundedLinearOperators (Y,Z);
set G = R_NormSpace_of_BoundedLinearOperators (X,Z);
defpred S₁[ object , object ] means ex u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) ex v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) st
( $1 = [u,v] & $2 = v * u );
A1: for x being object st x in the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] holds
ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S₁[x,y] )

proof

let x be object ; :: thesis: ( x in the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] implies ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S₁[x,y] ) )
assume x in the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] ; :: thesis: ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S₁[x,y] )
then consider u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)), v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) such that
A2: x = [u,v] by PRVECT_3:18;
take y = v * u; :: thesis: ( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S₁[x,y] )
thus ( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S₁[x,y] ) by A2; :: thesis: verum

end;

consider L being Function of the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):], the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) such that
A3: for x being object st x in the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] holds
S₁[x,L . x] from FUNCT_2:sch 1(A1);
A4: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (u,v) = v * u

proof

let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (u,v) = v * u
let v be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: L . (u,v) = v * u
consider u1 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)), v1 being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) such that
A5: ( [u,v] = [u1,v1] & L . [u,v] = v1 * u1 ) by A3;
( u = u1 & v = v1 ) by A5, XTUPLE_0:1;
hence L . (u,v) = v * u by A5; :: thesis: verum

end;

A6: for x1, x2 being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))

proof

let x1, x2 be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
let y be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: L . ((x1 + x2),y) = (L . (x1,y)) + (L . (x2,y))
thus L . ((x1 + x2),y) = y * (x1 + x2) by A4
.= (y * x1) + (y * x2) by LM100
.= (L . (x1,y)) + (y * x2) by A4
.= (L . (x1,y)) + (L . (x2,y)) by A4 ; :: thesis: verum

end;

A7: for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for a being Real holds L . ((a * x),y) = a * (L . (x,y))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for a being Real holds L . ((a * x),y) = a * (L . (x,y))
let y be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: 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 A4
.= (a * y) * x by LOPBAN1624
.= a * (y * x) by LOPBAN1624
.= a * (L . (x,y)) by A4 ; :: thesis: verum

end;

A8: for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for y1, y2 being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for y1, y2 being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
let y1, y2 be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: L . (x,(y1 + y2)) = (L . (x,y1)) + (L . (x,y2))
thus L . (x,(y1 + y2)) = (y1 + y2) * x by A4
.= (y1 * x) + (y2 * x) by LM200
.= (L . (x,y1)) + (y2 * x) by A4
.= (L . (x,y1)) + (L . (x,y2)) by A4 ; :: thesis: verum

end;

for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))
let y be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: 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 A4
.= a * (y * x) by LOPBAN1624
.= a * (L . (x,y)) by A4 ; :: thesis: verum

end;

then reconsider L = L as BilinearOperator of (R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)),(R_NormSpace_of_BoundedLinearOperators (X,Z)) by A6, A7, A8, LOPBAN_8:12;
take L ; :: thesis: ( L is_continuous_on the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (u,v) = v * u ) )
set K = 1;
for x being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.||

proof

let x be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for y being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.||
let y be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.||
L . (x,y) = y * x by A4;
hence ||.(L . (x,y)).|| <= (1 * ||.x.||) * ||.y.|| by NRM; :: thesis: verum

end;

hence ( L is_continuous_on the carrier of [:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):] & ( for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (u,v) = v * u ) ) by A4, LOPBAN_8:13; :: thesis: verum