let M be MidSp; 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
A3:
for p, q, r being Point of M st (vect M) . (p,q) = (vect M) . (p,r) holds
q = r
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;
((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
;
verum
end;
hence
vect M is_atlas_of the carrier of M, vectgroup M
by A1, A3; verum