theorem ch4: :: FIELD_9:6

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