:: deftheorem defines R_NormSpace_of_BoundedBilinearOperators LOPBAN_9:def 9 :
for X, Y, Z being RealNormSpace holds R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) = NORMSTR(# (BoundedBilinearOperators (X,Y,Z)),(Zero_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Add_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(Mult_ ((BoundedBilinearOperators (X,Y,Z)),(R_VectorSpace_of_BilinearOperators (X,Y,Z)))),(BoundedBilinearOperatorsNorm (X,Y,Z)) #);