environ
vocabularies HIDDEN, NUMBERS, BHSP_1, FINSET_1, SUBSET_1, RLVECT_1, RLVECT_3, XBOOLE_0, RLVECT_2, CARD_3, TARSKI, FUNCT_1, CARD_1, FINSEQ_1, STRUCT_0, RELAT_1, VALUED_1, FINSEQ_4, ORDINAL4, ARYTM_1, ARYTM_3, XXREAL_0, RLSUB_1, RLVECT_5, NAT_1, SUPINF_2, FUNCT_2, RLSUB_2, REAL_1, ALGSTR_0, RUSUB_4;
notations HIDDEN, TARSKI, XBOOLE_0, ENUMSET1, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, NAT_1, FINSEQ_1, FUNCT_1, FUNCT_2, DOMAIN_1, STRUCT_0, ALGSTR_0, RLVECT_1, FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_1, RLVECT_2, BHSP_1, RLVECT_3, RUSUB_1, RUSUB_2, RUSUB_3, XXREAL_0;
definitions TARSKI;
theorems FUNCT_1, FINSEQ_1, FINSEQ_2, FINSEQ_3, FINSEQ_4, FINSET_1, RLSUB_2, RLVECT_1, RLVECT_2, TARSKI, XBOOLE_0, XBOOLE_1, RUSUB_1, RUSUB_2, RLVECT_3, ENUMSET1, RLVECT_5, NAT_1, SUBSET_1, RUSUB_3, RLSUB_1, CARD_1, CARD_2, XCMPLX_0, XCMPLX_1, XREAL_1, XXREAL_0, STRUCT_0, ZFMISC_1;
schemes NAT_1, XBOOLE_0, FINSEQ_1, DOMAIN_1;
registrations SUBSET_1, RELSET_1, FINSET_1, XREAL_0, NAT_1, FINSEQ_1, STRUCT_0, RLVECT_1, RLSUB_1, RLVECT_3, ORDINAL1, CARD_1, RLVECT_2;
constructors HIDDEN, XXREAL_0, REAL_1, NAT_1, PARTFUN1, FINSEQ_3, FINSEQ_4, REALSET1, RLVECT_2, RLVECT_3, RUSUB_2, RUSUB_3, RELSET_1;
requirements HIDDEN, REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, STRUCT_0;
expansions XBOOLE_0, TARSKI, STRUCT_0;
Lm1:
for X, x being set st x in X holds
(X \ {x}) \/ {x} = X
Lm2:
for V being finite-dimensional RealUnitarySpace
for n being Element of NAT st n <= dim V holds
ex W being strict Subspace of V st dim W = n