let M be MidSp; :: thesis: for a, b, c being Element of M holds (vect (a,b)) + (vect (b,c)) = vect (a,c)
let a, b, c be Element of M; :: thesis: (vect (a,b)) + (vect (b,c)) = vect (a,c)
set p = [a,b];
set q = [b,c];
set u = [a,b] ~ ;
set v = [b,c] ~ ;
[a,b] `2 = b
.= [b,c] `1 ;
then ( [b,c] `2 = c & ([a,b] ~) + ([b,c] ~) = [([a,b] `1),([b,c] `2)] ~ ) by Def9;
hence (vect (a,b)) + (vect (b,c)) = vect (a,c) ; :: thesis: verum