theorem Th23: :: VECTSP_2:23

for R being Ring
for x, y being Scalar of R
for v, w being Vector of (LeftModule R) holds
( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )