thus
( F is Fanoian implies (1. F) + (1. F) <> 0. F )
; :: thesis: ( (1. F) + (1. F) <> 0. F implies F is Fanoian )

assume A1: (1. F) + (1. F) <> 0. F ; :: thesis: F is Fanoian

let a be Element of F; :: according to VECTSP_1:def 17 :: thesis: ( a + a = 0. F implies a = 0. F )

assume A2: a + a = 0. F ; :: thesis: a = 0. F

a = (1. F) * a ;

then a + a = ((1. F) + (1. F)) * a by Def7;

hence a = 0. F by A1, A2, Th8; :: thesis: verum

assume A1: (1. F) + (1. F) <> 0. F ; :: thesis: F is Fanoian

let a be Element of F; :: according to VECTSP_1:def 17 :: thesis: ( a + a = 0. F implies a = 0. F )

assume A2: a + a = 0. F ; :: thesis: a = 0. F

a = (1. F) * a ;

then a + a = ((1. F) + (1. F)) * a by Def7;

hence a = 0. F by A1, A2, Th8; :: thesis: verum