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