environ
vocabularies HIDDEN, NUMBERS, FINSEQ_1, SUBSET_1, RLVECT_1, REAL_1, STRUCT_0, FUNCT_1, XBOOLE_0, ALGSTR_0, RELAT_1, PARTFUN1, ARYTM_3, CARD_3, ORDINAL4, XXREAL_0, TARSKI, CARD_1, SUPINF_2, ARYTM_1, NAT_1, FUNCT_2, FINSET_1, FUNCOP_1, VALUED_1, RLSUB_1, QC_LANG1, BINOP_1, ZFMISC_1, RLVECT_2, LATTICES, VECTSP_1, PRE_POLY, FUNCT_7;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, FINSET_1, FINSEQ_1, RELAT_1, FUNCT_1, RELSET_1, PRE_POLY, PARTFUN1, FUNCT_2, FUNCOP_1, DOMAIN_1, VALUED_1, FINSEQ_4, STRUCT_0, ALGSTR_0, GROUP_1, RLVECT_1, VECTSP_1, REAL_1, RLSUB_1, NAT_1, BINOP_1, XXREAL_0;
definitions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, RLVECT_1, FUNCT_2, ALGSTR_0;
theorems CARD_1, CARD_2, ENUMSET1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FUNCT_1, FUNCT_2, NAT_1, RLSUB_1, RLSUB_2, RLVECT_1, TARSKI, ZFMISC_1, RELAT_1, XBOOLE_0, XBOOLE_1, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, ORDINAL1, PARTFUN1, VALUED_1, XREAL_0, VECTSP_1, PRE_POLY;
schemes BINOP_1, FINSEQ_1, FUNCT_2, NAT_1, XBOOLE_0;
registrations SUBSET_1, FUNCT_1, RELSET_1, FUNCT_2, FINSET_1, NUMBERS, XREAL_0, STRUCT_0, RLVECT_1, RLSUB_1, VALUED_1, VALUED_0, MEMBERED, FINSEQ_1, CARD_1, VECTSP_1, ORDINAL1;
constructors HIDDEN, PARTFUN1, BINOP_1, DOMAIN_1, FUNCOP_1, XXREAL_0, REAL_1, NAT_1, FINSEQ_4, RLSUB_1, VALUED_1, RELSET_1, VECTSP_1, PRE_POLY, RLVECT_1, NUMBERS, GROUP_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, BINOP_1, RLVECT_1, RELAT_1, STRUCT_0, ALGSTR_0;
expansions FUNCT_1, RLSUB_1, TARSKI, XBOOLE_0, BINOP_1, FUNCT_2, STRUCT_0;
reconsider zz = 0 as Element of REAL by XREAL_0:def 1;
Lm2:
for V being RealLinearSpace holds Sum (ZeroLC V) = 0. V