let AFV be WeakAffVect; for a, b, c, d, d9 being Element of AFV st a,b // c,d & a,b // c,d9 holds
d = d9
let a, b, c, d, d9 be Element of AFV; ( a,b // c,d & a,b // c,d9 implies d = d9 )
assume
( a,b // c,d & a,b // c,d9 )
; d = d9
then
( c,d // a,b & c,d9 // a,b )
by Th3;
then
c,d // c,d9
by Def1;
hence
d = d9
by Th4; verum