let M be MidSp; :: thesis:
set w = vect M;
A1: for p being Point of M
for x being Element of (vectgroup M) ex q being Point of M st (vect M) . (p,q) = x

let p be Point of M; :: thesis:
let x be Element of (vectgroup M); :: thesis:
reconsider xx = x as Vector of M by Th15;
consider q being Point of M such that
A2: xx = vect (p,q) by MIDSP_1:35;
take q ; :: thesis:
thus (vect M) . (p,q) = x by A2, Def8; :: thesis:

end;

A3: for p, q, r being Point of M st (vect M) . (p,q) = (vect M) . (p,r) holds
q = r

let p, q, r be Point of M; :: thesis:
assume (vect M) . (p,q) = (vect M) . (p,r) ; :: thesis:
then vect (p,q) = (vect M) . (p,r) by Def8
.= vect (p,r) by Def8 ;
hence q = r by MIDSP_1:39; :: thesis:

end;

for p, q, r being Point of M holds ((vect M) . (p,q)) + ((vect M) . (q,r)) = (vect M) . (p,r)

let p, q, r be Point of M; :: thesis:
( (vect M) . (p,q) = vect (p,q) & (vect M) . (q,r) = vect (q,r) ) by Def8;
hence ((vect M) . (p,q)) + ((vect M) . (q,r)) = (vect (p,q)) + (vect (q,r)) by Th15
.= vect (p,r) by MIDSP_1:40
.= (vect M) . (p,r) by Def8 ;
:: thesis:

end;