consider a1 being Vector of V such that
A6: S1 = a1 .. W by Th12;
consider a2 being Vector of V such that
A7: S2 = a2 .. W by Th12;

A8: now :: thesis: for b1, b2 being Vector of V st S1 = b1 .. W & S2 = b2 .. W holds
(a1 + a2) .. W = (b1 + b2) .. W

let b1, b2 be Vector of V; :: thesis: ( S1 = b1 .. W & S2 = b2 .. W implies (a1 + a2) .. W = (b1 + b2) .. W )
assume that
A9: S1 = b1 .. W and
A10: S2 = b2 .. W ; :: thesis: (a1 + a2) .. W = (b1 + b2) .. W
A11: a1 - b1 in W by A6, A9, Th11;
a2 - b2 in W by A7, A10, Th11;
then A12: (a1 - b1) + (a2 - b2) in W by A11, VECTSP_4:20;
(a1 - b1) + (a2 - b2) = ((a1 - b1) + a2) - b2 by RLVECT_1:def 3
.= ((a1 + a2) - b1) - b2 by Lm1
.= (a1 + a2) - (b1 + b2) by VECTSP_1:17 ;
hence (a1 + a2) .. W = (b1 + b2) .. W by A12, Th11; :: thesis: verum

end;

take (a1 + a2) .. W ; :: thesis: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
(a1 + a2) .. W = (a1 + a2) .. W
thus for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds
(a1 + a2) .. W = (a1 + a2) .. W by A8; :: thesis: verum