let S, T be Element of V .. W; :: thesis: ( ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

S = (a1 + a2) .. W ) & ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

T = (a1 + a2) .. W ) implies S = T )

assume that

A13: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

S = (a1 + a2) .. W and

A14: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

T = (a1 + a2) .. W ; :: thesis: S = T

consider a1 being Vector of V such that

A15: S1 = a1 .. W by Th12;

consider a2 being Vector of V such that

A16: S2 = a2 .. W by Th12;

thus S = (a1 + a2) .. W by A13, A15, A16

.= T by A14, A15, A16 ; :: thesis: verum

S = (a1 + a2) .. W ) & ( for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

T = (a1 + a2) .. W ) implies S = T )

assume that

A13: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

S = (a1 + a2) .. W and

A14: for a1, a2 being Vector of V st S1 = a1 .. W & S2 = a2 .. W holds

T = (a1 + a2) .. W ; :: thesis: S = T

consider a1 being Vector of V such that

A15: S1 = a1 .. W by Th12;

consider a2 being Vector of V such that

A16: S2 = a2 .. W by Th12;

thus S = (a1 + a2) .. W by A13, A15, A16

.= T by A14, A15, A16 ; :: thesis: verum