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