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