consider a1 being Vector of V such that

A1: S1 = a1 .. W by Th12;

(- a1) .. W = (- a) .. W

thus for a being Vector of V st S1 = a .. W holds

(- a1) .. W = (- a) .. W by A2; :: thesis: verum

A1: S1 = a1 .. W by Th12;

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

(- a1) .. W = (- a) .. W

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

(- a1) .. W = (- a) .. W

thus for a being Vector of V st S1 = a .. W holds

(- a1) .. W = (- a) .. W by A2; :: thesis: verum