let X, Y, Z be RealNormSpace; :: thesis: for f being Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z))
for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds a * (f * g) = (a * f) * g
let f be Element of (R_NormSpace_of_BoundedLinearOperators (Y,Z)); :: thesis: for g being Element of (R_NormSpace_of_BoundedLinearOperators (X,Y))
for a being Real holds a * (f * g) = (a * f) * g
let g be Element of (R_NormSpace_of_BoundedLinearOperators (X,Y)); :: thesis: for a being Real holds a * (f * g) = (a * f) * g
let a be Real; :: thesis: a * (f * g) = (a * f) * g
reconsider jj = 1 as Real ;
a * (f * g) = (a * jj) * (f * g)
.= (a * f) * (jj * g) by LPB2Th11 ;
hence a * (f * g) = (a * f) * g by RLVECT_1:def 8; :: thesis: verum