let K be Field; :: 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 A1, VECTSP_1:def 18; :: 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 by VECTSP_1:def 18;
a = a * (1_ K) by VECTSP_1:def 4;
then 0. K = a * ((1_ K) + (1_ K)) by A3, VECTSP_1:def 7;
then 0. K = (1_ K) + (1_ K) by A4, VECTSP_1:12;
hence contradiction by A2, VECTSP_1:16; :: thesis: verum