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

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