theorem :: AFVECT0:42

for AFV being WeakAffVect
for o being Element of AFV holds
( the carrier of (GroupVect (AFV,o)) = the carrier of AFV & the addF of (GroupVect (AFV,o)) = Padd o & 0. (GroupVect (AFV,o)) = o ) ;