let X, Y, Z be RealNormSpace; :: thesis: for u being Point of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (- w) * (- u) = w * u
let u be Point of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for w being Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)) holds (- w) * (- u) = w * u
let w be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: (- w) * (- u) = w * u
thus (- w) * (- u) = - (w * (- u)) by LOPBAN1623
.= - (- (w * u)) by LOPBAN1623
.= w * u by RLVECT_1:17 ; :: thesis: verum