theorem XXXX: :: LOPBAN13:30

for X, Y being RealNormSpace
for v being Lipschitzian LinearOperator of X,Y
for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real st v = w holds
a * w = a (#) v