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

set G = vectgroup M;
set p = the Point of M;
thus for a being Element of () ex x being Element of () st Double x = a :: thesis: for a being Element of () st Double a = 0. () holds
a = 0. ()
proof
set p = the Point of M;
let a be Element of (); :: thesis: ex x being Element of () 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 () 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 ;
hence Double x = a by Th15; :: thesis: verum
end;
let a be Element of (); :: thesis: ( Double a = 0. () implies a = 0. () )
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. () ; :: thesis: a = 0. ()
then aa + aa = 0. () 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 ;
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 ;
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 ;
hence a = ID M by
.= 0. () by Th15 ;
:: thesis: verum