let AFV be WeakAffVect; :: thesis: for a, b, p being Element of AFV st a,b '||' p,p holds
a = b
let a, b, p be Element of AFV; :: thesis: ( a,b '||' p,p implies a = b )
assume a,b '||' p,p ; :: thesis: a = b
then a,b // p,p by DIRAF:def 4;
hence a = b by AFVECT0:def 1; :: thesis: verum