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) & (- 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) & (- w) * u = - (w * u) )
let w be Point of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: ( w * (- u) = - (w * u) & (- w) * u = - (w * u) )
for x being Point of X holds (w * (- u)) . x = (- 1) * ((w * u) . x)

proof

let x be Point of X; :: thesis: (w * (- u)) . x = (- 1) * ((w * u) . x)
thus (w * (- u)) . x = (modetrans (w,Y,Z)) . ((modetrans ((- u),X,Y)) . x) by FUNCT_2:15
.= (modetrans (w,Y,Z)) . ((- u) . x) by LOPBAN_1:def 11
.= (modetrans (w,Y,Z)) . (((- 1) * u) . x) by RLVECT_1:16
.= (modetrans (w,Y,Z)) . ((- 1) * (u . x)) by LOPBAN_1:36
.= (- 1) * ((modetrans (w,Y,Z)) . (u . x)) by LOPBAN_1:def 5
.= (- 1) * ((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) by LOPBAN_1:def 11
.= (- 1) * ((w * u) . x) by FUNCT_2:15 ; :: thesis: verum

end;

hence w * (- u) = (- 1) * (w * u) by LOPBAN_1:36
.= - (w * u) by RLVECT_1:16 ;
:: thesis: (- w) * u = - (w * u)
for x being Point of X holds ((- w) * u) . x = (- 1) * ((w * u) . x)

proof

let x be Point of X; :: thesis: ((- w) * u) . x = (- 1) * ((w * u) . x)
thus ((- w) * u) . x = (modetrans ((- w),Y,Z)) . ((modetrans (u,X,Y)) . x) by FUNCT_2:15
.= (- w) . ((modetrans (u,X,Y)) . x) by LOPBAN_1:def 11
.= ((- 1) * w) . ((modetrans (u,X,Y)) . x) by RLVECT_1:16
.= (- 1) * (w . ((modetrans (u,X,Y)) . x)) by LOPBAN_1:36
.= (- 1) * ((modetrans (w,Y,Z)) . ((modetrans (u,X,Y)) . x)) by LOPBAN_1:def 11
.= (- 1) * ((w * u) . x) by FUNCT_2:15 ; :: thesis: verum

end;

hence (- w) * u = (- 1) * (w * u) by LOPBAN_1:36
.= - (w * u) by RLVECT_1:16 ;
:: thesis: verum