let R be Ring; :: thesis: for x, y being Scalar of R
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 )
set MLT = the multF of R;
set LS = RightModStr(# the carrier of R, the addF of R,(0. R), the multF of R #);
for x, y being Scalar of R
for v, w being Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of 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 )

proof

let x, y be Scalar of R; :: thesis: for v, w being Vector of RightModStr(# the carrier of R, the addF of R,(0. R), the multF of 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 RightModStr(# the carrier of R, the addF of R,(0. R), the multF of 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 )
reconsider v9 = v, w9 = w as Scalar of R ;
thus (v + w) * x = (v9 + w9) * x
.= (v9 * x) + (w9 * x) by VECTSP_1:def 7
.= (v * x) + (w * x) ; :: thesis: ( v * (x + y) = (v * x) + (v * y) & v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (x + y) = v9 * (x + y)
.= (v9 * x) + (v9 * y) by VECTSP_1:def 7
.= (v * x) + (v * y) ; :: thesis: ( v * (y * x) = (v * y) * x & v * (1_ R) = v )
thus v * (y * x) = v9 * (y * x)
.= (v9 * y) * x by GROUP_1:def 3
.= (v * y) * x ; :: thesis: v * (1_ R) = v
thus v * (1_ R) = v9 * (1_ R)
.= v ; :: thesis: verum

end;

hence for x, y being Scalar of R
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 ) ; :: thesis: verum