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