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