take LeftModule R ; :: thesis: ( LeftModule R is VectSp-like & LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
thus 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 ) by Th71; :: according to VECTSP_1:def 26 :: thesis: ( LeftModule R is Abelian & LeftModule R is add-associative & LeftModule R is right_zeroed & LeftModule R is right_complementable & LeftModule R is strict )
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: verum