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