let M be MidSp; 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; (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)
; verum