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