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

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