set y = u + v;
set w = (2 ") * (u + v);
(2 ") + (2 ") = 1 ;
then ((2 ") * (u + v)) + ((2 ") * (u + v)) = 1 * (u + v) by RLVECT_1:def 9
.= u + v by RLVECT_1:def 11 ;
hence ex b₁ being VECTOR of V st b₁ + b₁ = u + v ; :: thesis: verum