let X, Y be RealNormSpace; :: thesis: 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
let v be Lipschitzian LinearOperator of X,Y; :: thesis: for w being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real st v = w holds
- w = - v
let w be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for a being Real st v = w holds
- w = - v
let a be Real; :: thesis: ( v = w implies - w = - v )
assume A1: v = w ; :: thesis: - w = - v
thus - w = (- 1) * w by RLVECT_1:16
.= (- 1) (#) v by A1, XXXX
.= - v by VFUNCT_1:23 ; :: thesis: verum