let R be Ring; :: thesis: RightModule R is RightMod-like
let x, y be Scalar of R; :: according to VECTSP_2:def 9 :: thesis: for v, w being Vector of (RightModule R) holds
( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
let v, w be Vector of (RightModule R); :: thesis: ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus ( (v + w) * x = (v * x) + (w * x) & v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v ) by Th77; :: thesis: verum