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 Th27, Th41
.= vect (a,b) by Th40 ;
hence (vect (a,(a @ b))) + (vect (a,(a @ b))) = vect (a,b) ; :: thesis: verum