environ
vocabularies HIDDEN, FUNCT_1, RELAT_1, TARSKI, STRUCT_0, SUBSET_1, XBOOLE_0, VECTSP_1, RLVECT_5, FINSET_1, RLVECT_3, LOPBAN_1, ARYTM_3, SUPINF_2, CARD_1, RLSUB_1, FUNCT_2, ARYTM_1, MESFUNC1, VECTSP10, RLVECT_2, FUNCT_4, REALSET1, FUNCOP_1, QC_LANG1, CARD_3, RLSUB_2, FINSEQ_1, VALUED_1, NAT_1, XXREAL_0, PARTFUN1, PBOOLE, RANKNULL, MSSUBFAM, UNIALG_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, DOMAIN_1, RELAT_1, RELSET_1, FUNCT_1, ORDINAL1, NAT_1, NUMBERS, FUNCOP_1, PARTFUN1, FUNCT_2, FUNCT_4, XCMPLX_0, XXREAL_0, CARD_1, FINSET_1, FINSEQ_1, FINSEQOP, STRUCT_0, RLVECT_1, RLVECT_2, VECTSP_1, FUNCT_7, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MOD_2, MATRLIN, VECTSP_9, LOPBAN_1;
definitions TARSKI, FUNCT_1, XBOOLE_0, MATRLIN, FUNCT_2;
theorems TARSKI, ZFMISC_1, RELAT_1, FINSET_1, FINSEQ_1, FUNCT_1, VECTSP_7, VECTSP_9, CARD_2, XBOOLE_1, FUNCT_2, SUBSET_1, XBOOLE_0, VECTSP_1, RLVECT_1, VECTSP_4, VECTSP_6, RLVECT_2, MOD_2, MATRLIN, CARD_1, FUNCOP_1, VECTSP_5, FUNCT_7, FINSEQ_2, FUNCT_4, ENUMSET1, PARTFUN1;
schemes CLASSES1;
registrations RELAT_1, FUNCT_1, STRUCT_0, CARD_1, FINSET_1, VECTSP_9, XBOOLE_0, MATRLIN, FUNCOP_1, ORDINAL1, XREAL_0, SUBSET_1, RELSET_1;
constructors HIDDEN, NAT_1, FINSEQOP, HAHNBAN, VECTSP_6, VECTSP_7, MOD_2, VECTSP_9, REALSET1, RLVECT_2, WELLORD2, LOPBAN_1, VECTSP_5, FUNCT_7, FUNCT_4, XXREAL_0, MATRLIN, RELSET_1;
requirements HIDDEN, BOOLE, SUBSET, NUMERALS, ARITHM;
equalities RELAT_1, FINSEQ_1, VECTSP_4, VECTSP_6, RLVECT_1, STRUCT_0, LOPBAN_1;
expansions TARSKI, FUNCT_1, FINSEQ_1, VECTSP_4, XBOOLE_0, STRUCT_0;
Lm1:
for F being Field
for V being VectSp of F
for l being Linear_Combination of V
for X being Subset of V holds l .: X is finite
:: any subset of X.