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