let K be commutative Ring; :: thesis: ( not K is degenerated & K is well-unital & K is domRing-like implies ( K is Fanoian iff 1_ K <> - (1_ K) ) )
assume A0: ( not K is degenerated & K is well-unital & K is domRing-like ) ; :: thesis: ( K is Fanoian iff 1_ K <> - (1_ K) )
thus ( K is Fanoian implies 1_ K <> - (1_ K) ) :: thesis: ( 1_ K <> - (1_ K) implies K is Fanoian )
proof
assume A1: K is Fanoian ; :: thesis: 1_ K <> - (1_ K)
assume 1_ K = - (1_ K) ; :: thesis: contradiction
then (1_ K) + (1_ K) = 0. K by RLVECT_1:def 10;
hence contradiction by A0, A1; :: thesis: verum
end;
assume A2: 1_ K <> - (1_ K) ; :: thesis: K is Fanoian
assume not K is Fanoian ; :: thesis: contradiction
then consider a being Element of K such that
A3: a + a = 0. K and
A4: a <> 0. K ;
a = a * (1_ K) ;
then 0. K = a * ((1_ K) + (1_ K)) by A3, VECTSP_1:def 7;
then 0. K = (1_ K) + (1_ K) by A0, A4, VECTSP_2:def 1;
hence contradiction by A2, VECTSP_1:16; :: thesis: verum