theorem :: LOPBAN13:31

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
- w = - v