for AFV being AffVect
for o being Element of AFV holds GroupVect (AFV,o) is Proper_Uniquely_Two_Divisible_Group ;