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 Th38, RSSPACE3:2; :: thesis: verum