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 Th12;

thus S = (- a1) .. W by A3, A5

.= T by A4, A5 ; :: thesis: verum

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 Th12;

thus S = (- a1) .. W by A3, A5

.= T by A4, A5 ; :: thesis: verum