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;

(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

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

take
(a1 + a2) .. W
; :: thesis: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. 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;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

(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