theorem Th16: :: CLOPBAN1:16

for X, Y being ComplexLinearSpace
for f, h being VECTOR of (C_VectorSpace_of_LinearOperators (X,Y))
for c being Complex holds
( h = c * f iff for x being VECTOR of X holds h . x = c * (f . x) )