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

H: now :: thesis: ( 4 '*' a = 0. F implies a = 0. F )

assume 4 '*' a = 0. F ; :: thesis: a = 0. F
then 0. F = (2 * 2) '*' a
.= 2 '*' (2 '*' ((1. F) * a)) by RING_3:65
.= 2 '*' ((2 '*' (1. F)) * a) by REALALG2:5
.= 2 '*' (a * (2 '*' (1. F))) by GROUP_1:def 12
.= (2 '*' a) * (2 '*' (1. F)) by REALALG2:5 ;
then 2 '*' a = 0. F by I, VECTSP_2:def 1;
hence a = 0. F by ch2; :: thesis: verum

end;

now :: thesis: ( a = 0. F implies 4 '*' a = 0. F )

assume a = 0. F ; :: thesis: 4 '*' a = 0. F
then B: 2 '*' a = 0. F by ch2;
(2 + 2) '*' a = (2 '*' a) + (2 '*' a) by RING_3:62;
hence 4 '*' a = 0. F by B; :: thesis: verum

end;

hence ( 4 '*' a = 0. F iff a = 0. F ) by H; :: thesis: verum