let M be MidSp; ( ( 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
for a being Element of (vectgroup M) st Double a = 0. (vectgroup M) holds
a = 0. (vectgroup M)
let a be Element of (vectgroup M); ( Double a = 0. (vectgroup M) implies 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)
; 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
;
verum