let X be RealNormSpace; for f, g being Element of BoundedLinearOperators (X,X)
for a being Real holds a * (f * g) = (a * f) * g
let f, g be Element of BoundedLinearOperators (X,X); for a being Real holds a * (f * g) = (a * f) * g
let a be Real; a * (f * g) = (a * f) * g
set RRL = RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #);
reconsider jj = 1 as Real ;
reconsider gg = g as Element of RLSStruct(# (BoundedLinearOperators (X,X)),(Zero_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Add_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))),(Mult_ ((BoundedLinearOperators (X,X)),(R_VectorSpace_of_LinearOperators (X,X)))) #) ;
A1: jj * g =
jj * gg
.=
g
by RLVECT_1:def 8
;
a * (f * g) =
(a * jj) * (f * g)
.=
(a * f) * (jj * g)
by Th11
;
hence
a * (f * g) = (a * f) * g
by A1; verum