take F = F_Real ; :: thesis: F is Fanoian
let a be Element of F; :: according to VECTSP_1:def 28 :: thesis: ( a + a = 0. F implies a = 0. F )
assume A1: 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, Th44, Th78; :: thesis: verum