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

q = r

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

A3:
for p, q, r being Point of M st (vect M) . (p,q) = (vect M) . (p,r) holds
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;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

q = r

proof

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 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;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

proof

hence
vect M is_atlas_of the carrier of M, vectgroup M
by A1, A3; :: thesis: verum
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;( (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