let R be 0 -characteristic domRing; :: thesis: for a being Element of R holds
( - a = a iff a = 0. R )
let a be Element of R; :: thesis: ( - a = a iff a = 0. R )
hereby :: thesis: ( a = 0. R implies - a = a )
assume - a = a ; :: thesis: a = 0. R
then a + a = 0. R by RLVECT_1:5;
then C: 0. R = (1 '*' a) + a by RING_3:60
.= (1 '*' a) + (1 '*' a) by RING_3:60
.= (1 + 1) '*' a by RING_3:62 ;
Char R = 0 by RING_3:def 6;
then a is zero by C, char4;
hence a = 0. R ; :: thesis: verum
end;
thus ( a = 0. R implies - a = a ) ; :: thesis: verum