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