for AFV being WeakAffVect
for o being Element of AFV
for a being Element of (GroupVect (AFV,o))
for a9 being Element of AFV st a = a9 holds
- a = (Pcom o) . a9