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