environ
vocabularies HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, REALSET1, FUNCT_4, FINSET_1, CARD_1, PBOOLE, CARD_3, ARYTM_3, ARYTM_1, NUMBERS, XXREAL_0, REAL_1, NAT_1, INT_1, VALUED_0, ORDINAL4, GRCAT_1, MESFUNC1, MOD_3, CLASSES1, RFINSEQ, FINSEQ_1, VALUED_1, SUPINF_2, MSSUBFAM, STRUCT_0, RLVECT_1, RLSUB_1, RLSUB_2, RLVECT_2, RLVECT_3, RMOD_2, PRELAMB, UNIALG_1, MSAFREE2, RANKNULL, UPROOTS, VECTSP10, ZMODUL01, ZMODUL03, ZMODUL05, SETWISEO, BINOP_2, VECTSP_1, INT_3;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, CLASSES1, RELSET_1, PARTFUN1, FUNCT_2, DOMAIN_1, FUNCOP_1, FUNCT_4, FINSET_1, SETWOP_2, RFINSEQ, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, INT_1, VALUED_0, FINSEQ_1, FINSEQOP, RVSUM_1, FUNCT_7, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, GR_CY_1, VECTSP_1, MOD_2, GRCAT_1, RLVECT_2, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, INT_3, LOPBAN_1, VECTSP_7, ZMODUL01, ZMODUL02, ZMODUL03;
definitions TARSKI, XBOOLE_0, FUNCT_1, FUNCT_2, VECTSP_2, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MOD_2, RFINSEQ, CLASSES1;
theorems TARSKI, XBOOLE_0, XBOOLE_1, ENUMSET1, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, CARD_1, CLASSES1, NAT_1, INT_1, CARD_2, FINSEQ_1, FINSEQ_2, FINSEQOP, FINSEQ_3, FINSEQ_4, RVSUM_1, RFINSEQ, FUNCT_7, RLVECT_1, VECTSP_1, GR_CY_1, RANKNULL, ZMODUL01, ZMODUL02, ZMODUL03, ZMODUL04, FINSOP_1, VECTSP_5, VECTSP_7, VECTSP_4, VECTSP_6, MOD_2, INT_3;
schemes FUNCT_2, CLASSES1, NAT_1, FINSEQ_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, RELSET_1, FUNCT_2, FUNCOP_1, FINSET_1, CARD_1, NUMBERS, XREAL_0, NAT_1, INT_1, VALUED_0, FINSEQ_1, RVSUM_1, INT_6, STRUCT_0, RLVECT_1, GRCAT_1, ZMODUL01, ZMODUL02, MOD_2, ZMODUL03, ZMODUL04, BINOP_2, VECTSP_2, VECTSP_4, INT_3, ALGSTR_0;
constructors HIDDEN, RELSET_1, REALSET1, CLASSES1, FINSEQOP, FINSOP_1, FUNCT_7, ALGSTR_1, GR_CY_1, LOPBAN_1, ZMODUL02, ZMODUL03, SETWISEO, BINOP_2, VECTSP_2, VECTSP_4, VECTSP_6, VECTSP_7, INT_3, ALGSTR_0, RLVECT_2, REAL_1, VFUNCT_1, RFINSEQ, GRCAT_1, MOD_2, VECTSP_5, MOD_4, ZMODUL01;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM, REAL;
equalities FINSEQ_1, STRUCT_0, ALGSTR_0, LOPBAN_1, ZMODUL02, VECTSP_2, SUBSET_1, VECTSP_4, VECTSP_6, RELAT_1;
expansions TARSKI, XBOOLE_0, FINSEQ_1, STRUCT_0, VECTSP_1, ZMODUL02, ZMODUL03, VECTSP_2, VECTSP_4, MOD_2, VECTSP_6, VECTSP_7, RFINSEQ, CLASSES1;
RL5Lm2:
for V being free finite-rank Z_Module
for W being Submodule of V
for n being Nat st n <= rank V holds
ex W being strict free Submodule of V st rank W = n
Lm1:
for V being Z_Module
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
ThTF3C1:
for V, W being non empty set
for A being finite Subset of V
for l being Function of V,W holds
( l * (canFS A) is W -valued & l * (canFS A) is FinSequence-like )
RF9:
for R1, R2 being FinSequence of INT.Ring st R1,R2 are_fiberwise_equipotent holds
Sum R1 = Sum R2
::theorem
::: for X be finite Subset of INT st X = {}
::: holds Sum X = 0 by Def2,GR_CY_1:3,RELAT_1:38;
::theorem
:: for v be Element of INT holds Sum {v} = v
:: proof
:: let v be Element of INT;
:: A1: Sum <*v*> = v by RVSUM_1:73;
:: rng <*v*> = {v} & <*v*> is one-to-one by FINSEQ_1:39;
:: hence Sum {v} = v by A1,Def2;
:: end;
::theorem
:: for S, T being finite Subset of INT
:: st T misses S holds
:: Sum (T \/ S) = (Sum T) + (Sum S)
:: proof
:: let S, T be finite Subset of INT;
:: consider F being FinSequence of INT such that
:: A1: rng F = T \/ S and
:: A2: F is one-to-one & Sum (T \/ S) = Sum F by Def2;
:: consider G being FinSequence of INT such that
:: A3: rng G = T and
:: A4: G is one-to-one and
:: A5: Sum T = Sum G by Def2;
:: consider H being FinSequence of INT such that
:: A6: rng H = S and
:: A7: H is one-to-one and
:: A8: Sum S = Sum H by Def2;
:: set I = G ^ H;
:: reconsider G0 = G, H0 = H as real-valued FinSequence;
::: A9: Sum (G0 ^ H0) = Sum (G) + Sum (H) by RVSUM_1:75;
:: assume T misses S; then
:: A10: G ^ H is one-to-one by A3,A4,A6,A7,FINSEQ_3:91;
:: rng (G ^ H) = rng F by A1,A3,A6,FINSEQ_1:31;
:: hence Sum (T \/ S) = (Sum T) + (Sum S) by A2,A5,A8,A9,A10,RLVECT142;
:: end;