theorem Th1: :: AFVECT0:1

for AFV being WeakAffVect
for a, b being Element of AFV holds a,b // a,b