let R be Ring; :: thesis: for V being RightMod of R
for a being Scalar of R
for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
let V be RightMod of R; :: thesis: for a being Scalar of R
for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
let a be Scalar of R; :: thesis: for L1, L2 being Linear_Combination of V holds (L1 + L2) * a = (L1 * a) + (L2 * a)
let L1, L2 be Linear_Combination of V; :: thesis: (L1 + L2) * a = (L1 * a) + (L2 * a)
let v be Vector of V; :: according to RMOD_4:def 8 :: thesis: ((L1 + L2) * a) . v = ((L1 * a) + (L2 * a)) . v
thus ((L1 + L2) * a) . v = ((L1 + L2) . v) * a by Def10
.= ((L1 . v) + (L2 . v)) * a by Def9
.= ((L1 . v) * a) + ((L2 . v) * a) by VECTSP_1:def 7
.= ((L1 * a) . v) + ((L2 . v) * a) by Def10
.= ((L1 * a) . v) + ((L2 * a) . v) by Def10
.= ((L1 * a) + (L2 * a)) . v by Def9 ; :: thesis: verum