environ
vocabularies HIDDEN, NUMBERS, ALGSTR_0, STRUCT_0, SUBSET_1, BINOP_1, FUNCT_1, ZFMISC_1, XBOOLE_0, RELAT_1, REAL_1, ARYTM_3, SUPINF_2, FUNCT_5, MCART_1, ARYTM_1, CARD_1, FINSEQ_1, ORDINAL4, CARD_3, TARSKI, XXREAL_0, FUNCOP_1, NAT_1, VALUED_0, RLVECT_1, PARTFUN1, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FUNCOP_1, REAL_1, FINSEQ_1, NAT_1, FUNCT_3, FUNCT_5, FINSEQ_4, STRUCT_0, ALGSTR_0;
definitions FUNCT_1, TARSKI, STRUCT_0, ALGSTR_0;
theorems FUNCT_1, NAT_1, TARSKI, RELAT_1, STRUCT_0, XBOOLE_0, XBOOLE_1, FINSEQ_1, XCMPLX_0, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, ALGSTR_0, FINSEQ_3, XREAL_0;
schemes FINSEQ_1, FUNCT_2, NAT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, XREAL_0, NAT_1, STRUCT_0, ALGSTR_0, FINSEQ_1, CARD_1, RELAT_1;
constructors HIDDEN, BINOP_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, FINSEQ_1, FUNCT_3, FUNCT_5, ALGSTR_0, REALSET1, RELSET_1, FINSEQ_4, VALUED_0, XREAL_0;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities RELAT_1, ALGSTR_0;
expansions FUNCT_1, STRUCT_0;
Lm1:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, w being Element of V st v + w = 0. V holds
w + v = 0. V
Lm2:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v, u being Element of V ex w being Element of V st v + w = u
Lm3:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for u, w being Element of V holds - (u + w) = (- w) + (- u)
Lm4:
for V being non empty addLoopStr holds Sum (<*> the carrier of V) = 0. V
Lm5:
for V being non empty addLoopStr
for F being FinSequence-like PartFunc of NAT,V st len F = 0 holds
Sum F = 0. V
Lm6:
for V being non empty right_complementable add-associative right_zeroed addLoopStr
for v being Element of V holds Sum <*v*> = v