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