consider a1 being Vector of V such that
A1: S1 = a1 .. W by Th12;

A2: now :: thesis: for a being Vector of V st S1 = a .. W holds
(- a1) .. W = (- a) .. W

let a be Vector of V; :: thesis: ( S1 = a .. W implies (- a1) .. W = (- a) .. W )
assume S1 = a .. W ; :: thesis: (- a1) .. W = (- a) .. W
then a1 - a in W by A1, Th11;
then - (a1 - a) in W by VECTSP_4:22;
then (- a1) - (- a) in W by Lm1;
hence (- a1) .. W = (- a) .. W by Th11; :: thesis: verum

end;

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