environ
vocabularies HIDDEN, NUMBERS, VECTSP_1, RLSUB_1, NAT_1, XBOOLE_0, STRUCT_0, SUBSET_1, RLVECT_2, FINSEQ_1, FUNCT_2, RELAT_1, CARD_3, VALUED_1, FUNCT_1, PARTFUN1, SUPINF_2, ORDINAL4, TARSKI, ARYTM_3, ARYTM_1, CLASSES1, FINSET_1, RLVECT_3, CARD_1, XXREAL_0, FINSEQ_4, RLVECT_5, RLSUB_2;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, DOMAIN_1, STRUCT_0, FUNCT_1, PARTFUN1, FUNCT_2, NAT_1, FINSET_1, FINSEQ_1, FINSEQ_3, FINSEQ_4, CLASSES1, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_6, VECTSP_5, VECTSP_7, MATRLIN, XXREAL_0;
definitions TARSKI;
theorems TARSKI, ENUMSET1, SUBSET_1, NAT_1, CARD_1, CARD_2, FUNCT_1, FUNCT_2, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, RFINSEQ, RLVECT_1, VECTSP_1, VECTSP_4, VECTSP_5, VECTSP_6, VECTSP_7, MATRLIN, XBOOLE_0, XBOOLE_1, RLVECT_2, VECTSP_2, ZFMISC_1, XREAL_1, XXREAL_0, STRUCT_0, PARTFUN1, RELAT_1;
schemes NAT_1, FINSEQ_1, FUNCT_2;
registrations XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, VECTSP_1, VECTSP_7, MATRLIN, CARD_1, RELSET_1;
constructors HIDDEN, FINSEQ_4, XXREAL_0, NAT_1, REALSET1, RFINSEQ, VECTSP_5, VECTSP_6, VECTSP_7, CLASSES1, MATRLIN, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI;
Lm1:
for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
Lm2:
for GF being Field
for n being Nat
for V being finite-dimensional VectSp of GF st n <= dim V holds
ex W being strict Subspace of V st dim W = n
:: Preliminaries
::