let M be MidSp; :: thesis: ( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )
set GS = vectgroup M;
thus vectgroup M is add-associative :: thesis: ( vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )

proof

let x, y, z be Element of (vectgroup M); :: according to RLVECT_1:def 3 :: thesis: (x + y) + z = x + (y + z)
reconsider xx = x, yy = y, zz = z as Element of setvect M ;
thus (x + y) + z = (addvect M) . ((xx + yy),zz) by Def15
.= (xx + yy) + zz by Def15
.= xx + (yy + zz) by Th75
.= (addvect M) . (xx,(yy + zz)) by Def15
.= x + (y + z) by Def15 ; :: thesis: verum

end;

thus vectgroup M is right_zeroed :: thesis: ( vectgroup M is right_complementable & vectgroup M is Abelian )

proof

let x be Element of (vectgroup M); :: according to RLVECT_1:def 4 :: thesis: x + (0. (vectgroup M)) = x
reconsider xx = x as Element of setvect M ;
thus x + (0. (vectgroup M)) = x :: thesis: verum

proof

reconsider xxx = xx as Vector of M by Th71;
xx + (zerovect M) = xxx + (ID M) by Def14
.= x by Th64 ;
hence x + (0. (vectgroup M)) = x by Def15; :: thesis: verum

end;

end;

thus vectgroup M is right_complementable :: thesis: vectgroup M is Abelian

proof

let x be Element of (vectgroup M); :: according to ALGSTR_0:def 16 :: thesis: x is right_complementable
reconsider xx = x as Element of setvect M ;
reconsider w = (complvect M) . xx as Element of (vectgroup M) ;
take w ; :: according to ALGSTR_0:def 11 :: thesis: x + w = 0. (vectgroup M)
thus x + w = xx + ((complvect M) . xx) by Def15
.= 0. (vectgroup M) by Def16 ; :: thesis: verum

end;

thus vectgroup M is Abelian :: thesis: verum

proof

let x, y be Element of (vectgroup M); :: according to RLVECT_1:def 2 :: thesis: x + y = y + x
reconsider xx = x, yy = y as Element of setvect M ;
thus x + y = xx + yy by Def15
.= yy + xx by Th74
.= y + x by Def15 ; :: thesis: verum

end;