let M be MidSp; :: thesis: ( ( for a being set holds

( a is Element of (vectgroup M) iff a is Vector of M ) ) & 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)

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 (vectgroup M) iff a is Vector of M ) :: thesis: ( 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)

for x, y being Vector of M st a = x & b = y holds

a + b = x + y ) )

.= ID M by MIDSP_1:def 16 ; :: thesis: for a, b being Element of (vectgroup M)

for x, y being Vector of M st a = x & b = y holds

a + b = x + y

thus for a, b being Element of (vectgroup M)

for x, y being Vector of M st a = x & b = y holds

a + b = x + y :: thesis: verum

( a is Element of (vectgroup M) iff a is Vector of M ) ) & 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)

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 (vectgroup M) iff a is Vector of M ) :: thesis: ( 0. (vectgroup M) = ID M & ( for a, b being Element of (vectgroup M)

for x, y being Vector of M st a = x & b = y holds

a + b = x + y ) )

proof

thus 0. (vectgroup M) =
zerovect M
by MIDSP_1:55
let a be set ; :: thesis: ( a is Element of (vectgroup M) iff a is Vector of M )

( a is Element of (vectgroup M) iff a is Element of setvect M ) by MIDSP_1:53;

hence ( a is Element of (vectgroup M) iff a is Vector of M ) by MIDSP_1:48; :: thesis: verum

end;( a is Element of (vectgroup M) iff a is Element of setvect M ) by MIDSP_1:53;

hence ( a is Element of (vectgroup M) iff a is Vector of M ) by MIDSP_1:48; :: thesis: verum

.= ID M by MIDSP_1:def 16 ; :: thesis: for a, b being Element of (vectgroup M)

for x, y being Vector of M st a = x & b = y holds

a + b = x + y

thus for a, b being Element of (vectgroup M)

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 (vectgroup M); :: 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 (vectgroup M) . (a,b) by RLVECT_1:2

.= (addvect M) . (xx,yy) by A1, MIDSP_1:54

.= xx + yy by MIDSP_1:def 14

.= x + y by MIDSP_1:def 13 ; :: thesis: verum

end;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 (vectgroup M) . (a,b) by RLVECT_1:2

.= (addvect M) . (xx,yy) by A1, MIDSP_1:54

.= xx + yy by MIDSP_1:def 14

.= x + y by MIDSP_1:def 13 ; :: thesis: verum