let X, Y, Z be RealNormSpace; for f, h being VECTOR of (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z))
for a being Real holds
( h = a * f iff for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = a * (f . (x,y)) )
let f, h be VECTOR of (R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z)); for a being Real holds
( h = a * f iff for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = a * (f . (x,y)) )
let a be Real; ( h = a * f iff for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = a * (f . (x,y)) )
A1:
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is Subspace of R_VectorSpace_of_BilinearOperators (X,Y,Z)
by RSSPACE:11;
then reconsider f1 = f as VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (R_VectorSpace_of_BilinearOperators (X,Y,Z)) by A1, RLSUB_1:10;
hereby ( ( for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = a * (f . (x,y)) ) implies h = a * f )
assume A2:
h = a * f
;
for x being Element of X
for y being Element of Y holds h . (x,y) = a * (f . (x,y))let x be
Element of
X;
for y being Element of Y holds h . (x,y) = a * (f . (x,y))let y be
Element of
Y;
h . (x,y) = a * (f . (x,y))
h1 = a * f1
by A1, A2, RLSUB_1:14;
hence
h . (
x,
y)
= a * (f . (x,y))
by Th17;
verum
end;
assume
for x being Element of X
for y being Element of Y holds h . (x,y) = a * (f . (x,y))
; h = a * f
then
h1 = a * f1
by Th17;
hence
h = a * f
by A1, RLSUB_1:14; verum