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 Th20, Th28;

hence b = c by Th16; :: thesis: verum

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 Th20, Th28;

hence b = c by Th16; :: thesis: verum