reconsider a = a as Element of REAL by XREAL_0:def 1;

(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X) ;

hence (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X) ; :: thesis: verum

(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X) ;

hence (Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) . (a,f) is Element of BoundedLinearOperators (X,X) ; :: thesis: verum