:: deftheorem Def6 defines BilinearOperators LOPBAN_9:def 1 :
for X, Y, Z being RealLinearSpace
for b₄ being Subset of (RealVectSpace ( the carrier of [:X,Y:],Z)) holds
( b₄ = BilinearOperators (X,Y,Z) iff for x being set holds
( x in b₄ iff x is BilinearOperator of X,Y,Z ) );