let X, Y be RealNormSpace; :: thesis: R_NormSpace_of_BoundedLinearOperators X,Y is RealNormSpace
RLSStruct(# (BoundedLinearOperators X,Y),(Zero_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Add_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)),(Mult_ (BoundedLinearOperators X,Y),(R_VectorSpace_of_LinearOperators X,Y)) #) is RealLinearSpace ;
hence R_NormSpace_of_BoundedLinearOperators X,Y is RealNormSpace by Th44, RSSPACE3:4; :: thesis: verum