thus ( x is unital iff x divides 1. R ) :: thesis: verum

proof

hereby :: thesis: ( x divides 1. R implies x is unital )

assume x is unital ; :: thesis: x divides 1. R
hence x divides 1. R ; :: thesis: verum

end;

assume x divides 1. R ; :: thesis: x is unital
then ex y being Element of R st 1. R = x * y ;
hence x is unital ; :: thesis: verum

end;