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