let M be MidSp; :: thesis: ( ( for a being set holds
( a is Element of () iff a is Vector of M ) ) & 0. () = ID M & ( for a, b being Element of ()
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )

set G = vectgroup M;
thus for a being set holds
( a is Element of () iff a is Vector of M ) :: thesis: ( 0. () = ID M & ( for a, b being Element of ()
for x, y being Vector of M st a = x & b = y holds
a + b = x + y ) )
proof
let a be set ; :: thesis: ( a is Element of () iff a is Vector of M )
( a is Element of () iff a is Element of setvect M ) by MIDSP_1:53;
hence ( a is Element of () iff a is Vector of M ) by MIDSP_1:48; :: thesis: verum
end;
thus 0. () = zerovect M by MIDSP_1:55
.= ID M by MIDSP_1:def 16 ; :: thesis: for a, b being Element of ()
for x, y being Vector of M st a = x & b = y holds
a + b = x + y

thus for a, b being Element of ()
for x, y being Vector of M st a = x & b = y holds
a + b = x + y :: thesis: verum
proof
let a, b be Element of (); :: thesis: for x, y being Vector of M st a = x & b = y holds
a + b = x + y

let x, y be Vector of M; :: thesis: ( a = x & b = y implies a + b = x + y )
assume A1: ( a = x & b = y ) ; :: thesis: a + b = x + y
reconsider xx = x, yy = y as Element of setvect M by MIDSP_1:48;
thus a + b = the addF of () . (a,b) by RLVECT_1:2
.= () . (xx,yy) by
.= xx + yy by MIDSP_1:def 14
.= x + y by MIDSP_1:def 13 ; :: thesis: verum
end;