reconsider z = z as Element of COMPLEX by XCMPLX_0:def 2;
(Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f) is Element of BoundedLinearOperators (X,X) ;
hence (Mult_ ((BoundedLinearOperators (X,X)),(C_VectorSpace_of_LinearOperators (X,X)))) . (z,f) is Element of BoundedLinearOperators (X,X) ; :: thesis: verum