for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o)) ex b being Element of (GroupVect (AFV,o)) st b + b = a