environ
vocabularies HIDDEN, TARSKI, RLVECT_1, FUNCT_1, ARYTM_1, RELAT_1, MATHMORP, SETFAM_1, ARYTM_3, ALGSTR_0, MORPH_01, ZFMISC_1, SUBSET_1, STRUCT_0, XBOOLE_0, REAL_1, SUPINF_2, VALUED_2;
notations HIDDEN, TARSKI, XBOOLE_0, ORDINAL1, SUBSET_1, SETFAM_1, FUNCT_1, FUNCT_2, XCMPLX_0, XREAL_0, REAL_1, STRUCT_0, ALGSTR_0, RLVECT_1, RUSUB_4, MATHMORP;
definitions TARSKI, XBOOLE_0;
theorems SUBSET_1, RLVECT_1, TARSKI, ZFMISC_1, XBOOLE_0, SETFAM_1, RUSUB_5, XBOOLE_1, FUNCT_2, RLVECT_4;
schemes FUNCT_2;
registrations SUBSET_1, RELSET_1, MEMBERED, STRUCT_0, RLVECT_1, XREAL_0;
constructors HIDDEN, SETFAM_1, REAL_1, RUSUB_4, RVSUM_1, RELSET_1, MATHMORP;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE;
equalities XBOOLE_0, RLVECT_1, RUSUB_4, MATHMORP;
expansions TARSKI, XBOOLE_0;
Lm1:
for E being non empty Abelian addLoopStr
for A, B being Subset of E holds A (+) B = B (+) A