:: deftheorem defines GroupVect AFVECT0:def 8 :
for AFV being WeakAffVect
for o being Element of AFV holds GroupVect (AFV,o) = addLoopStr(# the carrier of AFV,(Padd o),o #);