consider a1 being Vector of V such that
A1: S = a1 . W by Th15;

A2: now :: thesis: for a being Vector of V st S = a . W holds
(r * a) . W = (r * a1) . W

let a be Vector of V; :: thesis: ( S = a . W implies (r * a) . W = (r * a1) . W )
assume S = a . W ; :: thesis: (r * a) . W = (r * a1) . W
then a - a1 in W by A1, Th11;
then r * (a - a1) in W by VECTSP_4:21;
then (r * a) - (r * a1) in W by VECTSP_1:23;
hence (r * a) . W = (r * a1) . W by Th11; :: thesis: verum

end;

take (r * a1) . W ; :: thesis: for a being Vector of V st S = a . W holds
(r * a1) . W = (r * a) . W
thus for a being Vector of V st S = a . W holds
(r * a1) . W = (r * a) . W by A2; :: thesis: verum