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 by MCART_1:7
.= [b,c] `1 by MCART_1:7 ;
then ( [b,c] `2 = c & ([a,b] ~ ) + ([b,c] ~ ) = [([a,b] `1 ),([b,c] `2 )] ~ ) by Def10, MCART_1:7;
hence (vect a,b) + (vect b,c) = vect a,c by MCART_1:7; :: thesis: verum