let M be MidSp; :: thesis: for u1, v1 being Element of setvect M holds u1 + v1 = v1 + u1
let u1, v1 be Element of setvect M; :: thesis: u1 + v1 = v1 + u1
reconsider u = u1, v = v1 as Vector of M by Th48;
thus u1 + v1 = u + v by Def13
.= v + u by Th46
.= v1 + u1 by Def13 ; :: thesis: verum