let X be RealNormSpace; :: thesis: 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); :: thesis: for a being Real holds a * (f * g) = (a * f) * g

let a be Real; :: thesis: 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; :: thesis: verum

for a being Real holds a * (f * g) = (a * f) * g

let f, g be Element of BoundedLinearOperators (X,X); :: thesis: for a being Real holds a * (f * g) = (a * f) * g

let a be Real; :: thesis: 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; :: thesis: verum