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

end;

hence for x, y being Scalar of
for v, w being Vector of 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