for a being Element of (GroupVect AFV,o) ex b being Element of (GroupVect AFV,o) st b + b = a by Th66;
hence GroupVect AFV,o is Two_Divisible by TDGROUP:def 1; :: thesis: verum