let R be Ring; :: thesis: for a being Scalar of R st - a = 0. R holds
a = 0. R
let a be Scalar of R; :: thesis: ( - a = 0. R implies a = 0. R )
assume - a = 0. R ; :: thesis: a = 0. R
then - (- a) = 0. R by RLVECT_1:12;
hence a = 0. R by RLVECT_1:17; :: thesis: verum