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: v1 + w1 = v + w by Def14;
u1 + v1 = u + v by Def14;
hence (u1 + v1) + w1 = (u + v) + w by Def14
.= u + (v + w) by Th63
.= u1 + (v1 + w1) by A1, Def14 ;
:: thesis: verum