theorem :: AFVECT0:45

for AFV being WeakAffVect
for o being Element of AFV holds 0. (GroupVect (AFV,o)) = o ;