theorem :: AFVECT0:10

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