let R be Ring; :: thesis: for V being RightMod of R
for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
let V be RightMod of R; :: thesis: for b, a being Scalar of R
for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
let b, a be Scalar of R; :: thesis: for L being Linear_Combination of V holds (L * b) * a = L * (b * a)
let L be Linear_Combination of V; :: thesis: (L * b) * a = L * (b * a)
let v be Vector of V; :: according to RMOD_4:def 8 :: thesis: ((L * b) * a) . v = (L * (b * a)) . v
thus ((L * b) * a) . v = ((L * b) . v) * a by Def12
.= ((L . v) * b) * a by Def12
.= (L . v) * (b * a) by GROUP_1:def 3
.= (L * (b * a)) . v by Def12 ; :: thesis: verum