let R be Ring; :: thesis: 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 )
set MLT = the multF of R;
set LS = ModuleStr(# 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 ModuleStr(# the carrier of R, the addF of R,(0. R), the multF of 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 )

proof

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

end;

hence 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 ) ; :: thesis: verum