let M be MidSp; :: thesis: vect M is_atlas_of the carrier of M, vectgroup M
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

proof

let p be Point of M; :: thesis: for x being Element of (vectgroup M) ex q being Point of M st (vect M) . (p,q) = x
let x be Element of (vectgroup M); :: thesis: ex q being Point of M st (vect M) . (p,q) = x
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: (vect M) . (p,q) = x
thus (vect M) . (p,q) = x by A2, Def8; :: thesis: verum

end;

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

proof

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

end;

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

proof

let p, q, r be Point of M; :: thesis: ((vect M) . (p,q)) + ((vect M) . (q,r)) = (vect M) . (p,r)
( (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: verum

end;

hence vect M is_atlas_of the carrier of M, vectgroup M by A1, A3; :: thesis: verum