let M be MidSp; :: thesis: vect M is associating
let p be Point of M; :: according to MIDSP_2:def 2 :: thesis: for q, r being Point of M holds
( p @ q = r iff (vect M) . (p,r) = (vect M) . (r,q) )
let q, r be Point of M; :: thesis: ( p @ q = r iff (vect M) . (p,r) = (vect M) . (r,q) )
set w = vect M;
( (vect M) . (p,r) = vect (p,r) & (vect M) . (r,q) = vect (r,q) ) by Def8;
hence ( p @ q = r iff (vect M) . (p,r) = (vect M) . (r,q) ) by Th23; :: thesis: verum