consider a1 being Vector of V such that

A1: S = a1 . W by Th15;

(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

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

take
(r * a1) . W
; :: 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;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

(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