let X, Y be RealNormSpace; :: thesis: for u, v being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)) holds u - (u + v) = - v
let u, v be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: u - (u + v) = - v
thus u - (u + v) = (u - u) - v by RLVECT_1:27
.= (0. (R_NormSpace_of_BoundedLinearOperators (X,Y))) - v by RLVECT_1:15
.= - v by RLVECT_1:14 ; :: thesis: verum