theorem :: AFVECT0:43

for AFV being WeakAffVect
for o being Element of AFV
for a, b being Element of (GroupVect (AFV,o))
for a9, b9 being Element of AFV st a = a9 & b = b9 holds
a + b = (Padd o) . (a9,b9) ;