let M be MidSp; :: thesis: for a, b, c being Element of M st vect a,b = vect a,c holds
b = c
let a, b, c be Element of M; :: thesis: ( vect a,b = vect a,c implies b = c )
assume vect a,b = vect a,c ; :: thesis: b = c
then ( a,b @@ a,b & a,b @@ a,c ) by Th32, Th43;
hence b = c by Th27; :: thesis: verum