let S, T be Element of V .. W; :: thesis: ( ( for a being Vector of V st S1 = a .. W holds
S = (- a) .. W ) & ( for a being Vector of V st S1 = a .. W holds
T = (- a) .. W ) implies S = T )
assume that
A3: for a being Vector of V st S1 = a .. W holds
S = (- a) .. W and
A4: for a being Vector of V st S1 = a .. W holds
T = (- a) .. W ; :: thesis: S = T
consider a1 being Vector of V such that
A5: S1 = a1 .. W by Th19;
thus S = (- a1) .. W by A3, A5
.= T by A4, A5 ; :: thesis: verum