let AFV be WeakAffVect; :: thesis: for a, b, c, d, d9 being Element of AFV st a,b // c,d & a,b // c,d9 holds
d = d9
let a, b, c, d, d9 be Element of AFV; :: thesis: ( a,b // c,d & a,b // c,d9 implies d = d9 )
assume ( a,b // c,d & a,b // c,d9 ) ; :: thesis: d = d9
then ( c,d // a,b & c,d9 // a,b ) by Th3;
then c,d // c,d9 by Def1;
hence d = d9 by Th4; :: thesis: verum