let M be MidSp; :: thesis: for u1, v1, w1 being Element of setvect M holds (u1 + v1) + w1 = u1 + (v1 + w1)
let u1, v1, w1 be Element of setvect M; :: thesis: (u1 + v1) + w1 = u1 + (v1 + w1)
reconsider u = u1, v = v1, w = w1 as Vector of M by Th71;
A1: u1 + v1 = u + v by Def14;
A2: v1 + w1 = v + w by Def14;
thus (u1 + v1) + w1 = (u + v) + w by A1, Def14
.= u + (v + w) by Th63
.= u1 + (v1 + w1) by A2, Def14 ; :: thesis: verum