let X, Y, Z be RealNormSpace; 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 S1[ 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)) & S1[x,y] )
proof
let x be
object ;
( 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)) & S1[x,y] ) )
assume
x in the
carrier of
[:(R_NormSpace_of_BoundedLinearOperators (X,Y)),(R_NormSpace_of_BoundedLinearOperators (Y,Z)):]
;
ex y being object st
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S1[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;
( y in the carrier of (R_NormSpace_of_BoundedLinearOperators (X,Z)) & S1[x,y] )
thus
(
y in the
carrier of
(R_NormSpace_of_BoundedLinearOperators (X,Z)) &
S1[
x,
y] )
by A2;
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
S1[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));
for v being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds L . (u,v) = v * ulet v be
Point of
(R_NormSpace_of_BoundedLinearOperators (Y,Z));
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;
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));
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));
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
;
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));
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));
for a being Real holds L . ((a * x),y) = a * (L . (x,y))let a be
Real;
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
;
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));
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));
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
;
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));
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));
for a being Real holds L . (x,(a * y)) = a * (L . (x,y))let a be
Real;
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
;
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
; ( 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.||
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; verum