let X, Y, Z be RealLinearSpace; for f, h being VECTOR of (R_VectorSpace_of_BilinearOperators (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_BilinearOperators (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)) )
reconsider f9 = f, h9 = h as BilinearOperator of X,Y,Z by Def6;
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_BilinearOperators (X,Y,Z) is Subspace of RealVectSpace ( the carrier of [:X,Y:],Z)
by RSSPACE:11;
then reconsider f1 = f as VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) by RLSUB_1:10;
reconsider h1 = h as VECTOR of (RealVectSpace ( the carrier of [:X,Y:],Z)) by A1, RLSUB_1:10;
A2:
now ( h = a * f implies for x being Element of X
for y being Element of Y holds h9 . (x,y) = a * (f9 . (x,y)) )assume A3:
h = a * f
;
for x being Element of X
for y being Element of Y holds h9 . (x,y) = a * (f9 . (x,y))let x be
Element of
X;
for y being Element of Y holds h9 . (x,y) = a * (f9 . (x,y))let y be
Element of
Y;
h9 . (x,y) = a * (f9 . (x,y))A4:
h1 = a * f1
by A1, A3, RLSUB_1:14;
[x,y] is
Element of
[:X,Y:]
;
hence
h9 . (
x,
y)
= a * (f9 . (x,y))
by A4, LOPBAN_1:2;
verum end;
now ( ( for x being Element of X
for y being Element of Y holds h9 . (x,y) = a * (f9 . (x,y)) ) implies h = a * f )end;
hence
( h = a * f iff for x being VECTOR of X
for y being VECTOR of Y holds h . (x,y) = a * (f . (x,y)) )
by A2; verum