let AFV be WeakAffVect; :: thesis: for a, b, a', b', c, d, d' being Element of 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 ; :: thesis: ( a,b // a',b' & c,d // b,a & c,d' // b',a' implies d = d' )
assume that
A1: a,b // a',b' and
A2: c,d // b,a and
A3: c,d' // b',a' ; :: thesis: d = d'
a',b' // a,b by A1, Th4;
then b',a' // b,a by Th8;
then c,d // b',a' by A2, Def1;
then c,d // c,d' by A3, Def1;
hence d = d' by Th5; :: thesis: verum