theorem :: AFVECT0:9

for AFV being WeakAffVect
for a, b, c, d, b9, c9, d9 being Element of AFV st b,c // b9,c9 & a,d // b,c & a,d9 // b9,c9 holds
d = d9