let M be MidSp; :: thesis: ( ( for a being Element of (vectgroup M) ex x being Element of (vectgroup M) st Double x = a ) & ( for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M) ) )
set G = vectgroup M;
thus for a being Element of (vectgroup M) ex x being Element of (vectgroup M) st Double x = a :: thesis: for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M)

proof

let a be Element of (vectgroup M); :: thesis: ex x being Element of (vectgroup M) st Double x = a
reconsider aa = a as Vector of M by Th18;
consider p being Point of M;
consider q being Point of M such that
A1: aa = vect p,q by MIDSP_1:55;
set xx = vect p,(p @ q);
A2: (vect p,(p @ q)) + (vect p,(p @ q)) = aa by A1, MIDSP_1:62;
reconsider x = vect p,(p @ q) as Element of (vectgroup M) by Th18;
take x ; :: thesis: Double x = a
thus Double x = a by A2, Th18; :: thesis: verum

end;

let a be Element of (vectgroup M); :: thesis: ( Double a = 0. (vectgroup M) implies a = 0. (vectgroup M) )
assume A3: Double a = 0. (vectgroup M) ; :: thesis: a = 0. (vectgroup M)
reconsider aa = a as Vector of M by Th18;
consider p being Point of M;
consider q being Point of M such that
A4: aa = vect p,q by MIDSP_1:55;
A5: aa + aa = 0. (vectgroup M) by A3, Th18
.= ID M by Th18 ;
consider r being Point of M such that
A6: aa = vect q,r by MIDSP_1:55;
(vect p,q) + (vect q,r) = vect p,p by A4, A5, A6, MIDSP_1:58;
then vect p,r = vect p,p by MIDSP_1:60;
then vect p,q = vect q,p by A4, A6, MIDSP_1:59;
then A7: p @ p = q @ q by MIDSP_1:57;
p = p @ p by MIDSP_1:def 4
.= q by A7, MIDSP_1:def 4 ;
hence a = ID M by A4, MIDSP_1:58
.= 0. (vectgroup M) by Th18 ;
:: thesis: verum