let R be Ring; :: thesis: LeftModule R is VectSp-like
let x, y be Scalar of R; :: according to VECTSP_1:def 26 :: thesis: for b₁, b₂ being Element of the carrier of (LeftModule R) holds
( x * (b₁ + b₂) = (x * b₁) + (x * b₂) & (x + y) * b₁ = (x * b₁) + (y * b₁) & (x * y) * b₁ = x * (y * b₁) & (1. R) * b₁ = b₁ )
let v, w be Vector of (LeftModule R); :: thesis: ( x * (v + w) = (x * v) + (x * w) & (x + y) * v = (x * v) + (y * v) & (x * y) * v = x * (y * v) & (1. R) * v = v )
thus ( 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; :: thesis: verum