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;

set p = the Point of 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)

reconsider aa = a as Vector of M by Th15;

consider q being Point of M such that

A2: aa = vect ( the Point of M,q) by MIDSP_1:35;

consider r being Point of M such that

A3: aa = vect (q,r) by MIDSP_1:35;

assume Double a = 0. (vectgroup M) ; :: thesis: a = 0. (vectgroup M)

then aa + aa = 0. (vectgroup M) by Th15

.= ID M by Th15 ;

then (vect ( the Point of M,q)) + (vect (q,r)) = vect ( the Point of M, the Point of M) by A2, A3, MIDSP_1:38;

then vect ( the Point of M,r) = vect ( the Point of M, the Point of M) by MIDSP_1:40;

then vect ( the Point of M,q) = vect (q, the Point of M) by A2, A3, MIDSP_1:39;

then A4: the Point of M @ the Point of M = q @ q by MIDSP_1:37;

the Point of M = the Point of M @ the Point of M by MIDSP_1:def 3

.= q by A4, MIDSP_1:def 3 ;

hence a = ID M by A2, MIDSP_1:38

.= 0. (vectgroup M) by Th15 ;

:: thesis: verum

a = 0. (vectgroup M) ) )

set G = vectgroup M;

set p = the Point of 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: ( Double a = 0. (vectgroup M) implies a = 0. (vectgroup M) )
set p = the Point of M;

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

consider q being Point of M such that

A1: aa = vect ( the Point of M,q) by MIDSP_1:35;

set xx = vect ( the Point of M,( the Point of M @ q));

reconsider x = vect ( the Point of M,( the Point of M @ q)) as Element of (vectgroup M) by Th15;

take x ; :: thesis: Double x = a

(vect ( the Point of M,( the Point of M @ q))) + (vect ( the Point of M,( the Point of M @ q))) = aa by A1, MIDSP_1:42;

hence Double x = a by Th15; :: thesis: verum

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

consider q being Point of M such that

A1: aa = vect ( the Point of M,q) by MIDSP_1:35;

set xx = vect ( the Point of M,( the Point of M @ q));

reconsider x = vect ( the Point of M,( the Point of M @ q)) as Element of (vectgroup M) by Th15;

take x ; :: thesis: Double x = a

(vect ( the Point of M,( the Point of M @ q))) + (vect ( the Point of M,( the Point of M @ q))) = aa by A1, MIDSP_1:42;

hence Double x = a by Th15; :: thesis: verum

reconsider aa = a as Vector of M by Th15;

consider q being Point of M such that

A2: aa = vect ( the Point of M,q) by MIDSP_1:35;

consider r being Point of M such that

A3: aa = vect (q,r) by MIDSP_1:35;

assume Double a = 0. (vectgroup M) ; :: thesis: a = 0. (vectgroup M)

then aa + aa = 0. (vectgroup M) by Th15

.= ID M by Th15 ;

then (vect ( the Point of M,q)) + (vect (q,r)) = vect ( the Point of M, the Point of M) by A2, A3, MIDSP_1:38;

then vect ( the Point of M,r) = vect ( the Point of M, the Point of M) by MIDSP_1:40;

then vect ( the Point of M,q) = vect (q, the Point of M) by A2, A3, MIDSP_1:39;

then A4: the Point of M @ the Point of M = q @ q by MIDSP_1:37;

the Point of M = the Point of M @ the Point of M by MIDSP_1:def 3

.= q by A4, MIDSP_1:def 3 ;

hence a = ID M by A2, MIDSP_1:38

.= 0. (vectgroup M) by Th15 ;

:: thesis: verum