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