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