let R be non 2 -characteristic domRing; :: thesis: for a being Element of R holds
( 2 '*' a = 0. R iff a = 0. R )
let a be Element of R; :: thesis: ( 2 '*' a = 0. R iff a = 0. R )
Char R <> 2 by RING_3:def 6;
then H: 2 '*' (1. R) <> 0. R by REALALG2:24;

A: now :: thesis: ( 2 '*' a = 0. R implies a = 0. R )

assume 2 '*' a = 0. R ; :: thesis: a = 0. R
then 0. R = 2 '*' ((1. R) * a)
.= (2 '*' (1. R)) * a by REALALG2:5 ;
hence a = 0. R by H, VECTSP_2:def 1; :: thesis: verum

end;

now :: thesis: ( a = 0. R implies 2 '*' a = 0. R )

assume B: a = 0. R ; :: thesis: 2 '*' a = 0. R
(1 + 1) '*' a = (1 '*' a) + (1 '*' a) by RING_3:62
.= (1 '*' a) + a by RING_3:60
.= a + a by RING_3:60 ;
hence 2 '*' a = 0. R by B; :: thesis: verum

end;

hence ( 2 '*' a = 0. R iff a = 0. R ) by A; :: thesis: verum