let R be Ring; :: thesis: ( LeftModule R is vector-distributive & LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
thus for x being Scalar of R
for v, w being Vector of (LeftModule R) holds x * (v + w) = (x * v) + (x * w) by Th71; :: according to VECTSP_1:def 14 :: thesis: ( LeftModule R is scalar-distributive & LeftModule R is scalar-associative & LeftModule R is scalar-unital )
thus for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x + y) * v = (x * v) + (y * v) by Th71; :: according to VECTSP_1:def 15 :: thesis: ( LeftModule R is scalar-associative & LeftModule R is scalar-unital )
thus for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x * y) * v = x * (y * v) by Th71; :: according to VECTSP_1:def 16 :: thesis: LeftModule R is scalar-unital
thus for v being Vector of (LeftModule R) holds (1. R) * v = v by Th71; :: according to VECTSP_1:def 17 :: thesis: verum