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)
; verum