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

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