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 11;
hence contradiction by A1, VECTSP_1:def 28; :: 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 & a <> 0. K ) by VECTSP_1:def 28;
a = a * (1_ K) by VECTSP_1:def 13;
then 0. K = a * ((1_ K) + (1_ K)) by A3, VECTSP_1:def 18;
then 0. K = (1_ K) + (1_ K) by A3, VECTSP_1:44;
hence contradiction by A2, VECTSP_1:63; :: thesis: verum