theorem ch2: :: FIELD_9:5

for R being non 2 -characteristic domRing
for a being Element of R holds
( 2 '*' a = 0. R iff a = 0. R )