let R be domRing; :: thesis: ( R is Field iff for a being NonUnit of R holds a = 0. R )

A: now :: thesis: ( R is Field implies for a being NonUnit of R holds a = 0. R )

assume R is Field ; :: thesis: for a being NonUnit of R holds a = 0. R
then B: R is almost_left_invertible ;
let a be NonUnit of R; :: thesis: a = 0. R

now :: thesis: not a <> 0. R

assume a <> 0. R ; :: thesis: contradiction
then consider b being Element of R such that
C: b * a = 1. R by B, ALGSTR_0:def 27;
a divides 1. R by C;
hence contradiction by GCD_1:def 20; :: thesis: verum

end;

hence a = 0. R ; :: thesis: verum

end;

now :: thesis: ( ( for a being NonUnit of R holds a = 0. R ) implies R is Field )

assume B: for a being NonUnit of R holds a = 0. R ; :: thesis: R is Field

now :: thesis: for a being Element of R st a <> 0. R holds
a is left_invertible

let a be Element of R; :: thesis: ( a <> 0. R implies a is left_invertible )
assume a <> 0. R ; :: thesis: a is left_invertible
then a is Unit of R by B;
then a divides 1. R by GCD_1:def 20;
then consider b being Element of R such that
C: a * b = 1. R ;
thus a is left_invertible by C; :: thesis: verum

end;

then R is almost_left_invertible ;
hence R is Field ; :: thesis: verum

end;

hence ( R is Field iff for a being NonUnit of R holds a = 0. R ) by A; :: thesis: verum