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