theorem Th4: :: AFVECT0:4

for AFV being WeakAffVect
for a, b, c being Element of AFV st a,b // a,c holds
b = c