environ
vocabularies HIDDEN, NUMBERS, FUNCSDOM, VECTSP_2, VECTSP_1, FINSEQ_1, NAT_1, SUBSET_1, FUNCT_1, FINSET_1, ARYTM_3, RELAT_1, CARD_3, XXREAL_0, TARSKI, CARD_1, STRUCT_0, SUPINF_2, PARTFUN1, XBOOLE_0, ORDINAL4, ARYTM_1, RLVECT_2, FUNCT_2, FUNCOP_1, VALUED_1, GROUP_1, RLSUB_1, FINSEQ_4, RLVECT_3, RMOD_2;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, FINSET_1, FINSEQ_1, ORDINAL1, NUMBERS, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, CARD_1, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, FINSEQ_4, VECTSP_2, RMOD_2, RMOD_3, FUNCOP_1, XXREAL_0;
definitions FUNCT_1, TARSKI, RMOD_2, XBOOLE_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, RLVECT_1, RLVECT_2, TARSKI, VECTSP_1, VECTSP_2, ZFMISC_1, RMOD_2, NAT_1, RELAT_1, XBOOLE_0, XBOOLE_1, RLSUB_2, XCMPLX_1, GROUP_1, FUNCOP_1, XREAL_1, PARTFUN1, STRUCT_0, RMOD_3;
schemes FINSEQ_1, FUNCT_2, NAT_1;
registrations XBOOLE_0, SUBSET_1, FUNCT_1, RELSET_1, FINSET_1, XREAL_0, STRUCT_0, VECTSP_1, ORDINAL1, FINSEQ_1, VECTSP_2, RMOD_2, CARD_1;
constructors HIDDEN, PARTFUN1, DOMAIN_1, FUNCOP_1, XXREAL_0, NAT_1, FINSEQ_4, RLVECT_2, RMOD_2, RMOD_3, RELSET_1;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET;
equalities RMOD_2, XBOOLE_0, RELAT_1;
expansions FUNCT_1, TARSKI, RMOD_2, XBOOLE_0;
Lm1:
for R being Ring
for V being RightMod of R
for v being Vector of V
for F, G being FinSequence of V st len F = (len G) + 1 & G = F | (Seg (len G)) & v = F . (len F) holds
Sum F = (Sum G) + v
Lm2:
for R being Ring
for V being RightMod of R
for a being Scalar of R
for F, G being FinSequence of V st len F = len G & ( for k being Nat st k in dom F holds
G . k = (F /. k) * a ) holds
Sum G = (Sum F) * a
Lm3:
for R being Ring
for V being RightMod of R holds Sum (ZeroLC V) = 0. V