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 Th18;
consider q being Point of M such that
A2: xx = vect p,q by MIDSP_1:55;
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:59; :: 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 Th18
.= vect p,r by MIDSP_1:60
.= (vect M) . p,r by Def8 ;
:: thesis: verum

end;

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