let X, Y, Z be RealNormSpace; :: thesis: R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace
R_VectorSpace_of_BoundedBilinearOperators (X,Y,Z) is RealLinearSpace ;
hence R_NormSpace_of_BoundedBilinearOperators (X,Y,Z) is RealNormSpace by RSSPACE3:2; :: thesis: verum