take LeftModule R ; :: thesis:
thus for x being Scalar of R
for v, w being Vector of (LeftModule R) holds x * (v + w) = (x * v) + (x * w) by Th23; :: according to VECTSP_1:def 13 :: thesis:
thus for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x + y) * v = (x * v) + (y * v) by Th23; :: according to VECTSP_1:def 14 :: thesis:
thus for x, y being Scalar of R
for v being Vector of (LeftModule R) holds (x * y) * v = x * (y * v) by Th23; :: according to VECTSP_1:def 15 :: thesis:
thus for v being Vector of (LeftModule R) holds (1. R) * v = v by Th23; :: according to VECTSP_1:def 16 :: thesis:
thus ( LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict ) ; :: thesis: