thus ( F is Fanoian implies (1. F) + (1. F) <> 0. F ) by Def30; :: 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 30 :: thesis: ( a + a = 0. F implies a = 0. F )
assume A2: a + a = 0. F ; :: thesis: a = 0. F
a = (1. F) * a by Def19;
then a + a = ((1. F) + (1. F)) * a by Def18;
hence a = 0. F by A1, A2, Th44; :: thesis: verum