let AFV be WeakAffVect; :: thesis: for a, b being Element of AFV holds a,b '||' b,a

let a, b be Element of AFV; :: thesis: a,b '||' b,a

a,b // a,b by AFVECT0:1;

hence a,b '||' b,a by DIRAF:def 4; :: thesis: verum

let a, b be Element of AFV; :: thesis: a,b '||' b,a

a,b // a,b by AFVECT0:1;

hence a,b '||' b,a by DIRAF:def 4; :: thesis: verum