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