let X be ComplexNormSpace; :: thesis: for f, g being Element of BoundedLinearOperators X,X
for a being Complex holds a * (f * g) = (a * f) * g
let f, g be Element of BoundedLinearOperators X,X; :: thesis: for a being Complex holds a * (f * g) = (a * f) * g
let a be Complex; :: thesis: a * (f * g) = (a * f) * g
set RRL = CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #);
reconsider gg = g as Element of CLSStruct(# (BoundedLinearOperators X,X),(Zero_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Add_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)),(Mult_ (BoundedLinearOperators X,X),(C_VectorSpace_of_LinearOperators X,X)) #) ;
A1: 1r * g = 1r * gg
.= g by CLVECT_1:def 2 ;
a * (f * g) = (a * 1r ) * (f * g) by COMPLEX1:def 7
.= (a * f) * (1r * g) by Th11 ;
hence a * (f * g) = (a * f) * g by A1; :: thesis: verum