for a being Element of (GroupVect (AFV,o)) st a + a = 0. (GroupVect (AFV,o)) holds
a = 0. (GroupVect (AFV,o)) by Th67;
hence GroupVect (AFV,o) is Fanoian by VECTSP_1:def 30; :: thesis: verum