let F be Field; :: thesis: for x, y being Element of F st x + y = 0. F holds
y = (comp F) . x
let x, y be Element of F; :: thesis: ( x + y = 0. F implies y = (comp F) . x )
assume x + y = 0. F ; :: thesis: y = (comp F) . x
then y = - x by RLVECT_1:6;
hence y = (comp F) . x by VECTSP_1:def 13; :: thesis: verum