let M be MidSp; :: thesis: for a, b being Element of M holds (vect a,(a @ b)) + (vect a,(a @ b)) = vect a,b
let a, b be Element of M; :: thesis: (vect a,(a @ b)) + (vect a,(a @ b)) = vect a,b
(vect a,(a @ b)) + (vect a,(a @ b)) = (vect a,(a @ b)) + (vect (a @ b),b) by Th42, Th61
.= vect a,b by Th60 ;
hence (vect a,(a @ b)) + (vect a,(a @ b)) = vect a,b ; :: thesis: verum