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