let M be MidSp; :: thesis: for u, v, w being Vector of M holds (u + v) + w = u + (v + w)
let u, v, w be Vector of M; :: thesis: (u + v) + w = u + (v + w)
consider a being Element of M;
consider b being Element of M such that
A1: u = vect (a,b) by Th55;
consider c being Element of M such that
A2: v = vect (b,c) by Th55;
consider d being Element of M such that
A3: w = vect (c,d) by Th55;
(u + v) + w = (vect (a,c)) + w by A1, A2, Th60
.= vect (a,d) by A3, Th60
.= (vect (a,b)) + (vect (b,d)) by Th60
.= u + (v + w) by A1, A2, A3, Th60 ;
hence (u + v) + w = u + (v + w) ; :: thesis: verum