for M being MidSp holds
( vectgroup M is add-associative & vectgroup M is right_zeroed & vectgroup M is right_complementable & vectgroup M is Abelian )