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)
set a = the Element of M;
consider b being Element of M such that
A1: u = vect ( the Element of M,b) by Th35;
consider c being Element of M such that
A2: v = vect (b,c) by Th35;
consider d being Element of M such that
A3: w = vect (c,d) by Th35;
(u + v) + w = (vect ( the Element of M,c)) + w by A1, A2, Th40
.= vect ( the Element of M,d) by A3, Th40
.= (vect ( the Element of M,b)) + (vect (b,d)) by Th40
.= u + (v + w) by A1, A2, A3, Th40 ;
hence (u + v) + w = u + (v + w) ; :: thesis: verum