environ
vocabularies HIDDEN, RLSUB_1, HAHNBAN, UNIALG_1, DUALSP01, INT_1, MOD_4, CARD_3, FINSET_1, RLVECT_1, ARYTM_1, RELAT_1, FUNCT_1, RSSPACE, REAL_1, TARSKI, MSSUBFAM, STRUCT_0, REALSET1, FCONT_1, SEQ_2, LOPBAN_1, ORDINAL2, ARYTM_3, ALGSTR_0, NORMSP_1, FUNCT_2, METRIC_1, PRE_TOPC, SUBSET_1, ZFMISC_1, ORDINAL1, NUMBERS, XBOOLE_0, CARD_1, SUPINF_2, COMPLEX1, XXREAL_0, NAT_1, RCOMP_1, NORMSP_2, RLVECT_3, NORMSP_3, RLVECT_2, TOPS_1, TOPGEN_1, RAT_1, DUALSP02, NORMSP_4;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, REALSET1, FINSET_1, CARD_1, CARD_3, NUMBERS, XCMPLX_0, XXREAL_0, RAT_1, XREAL_0, INT_1, COMPLEX1, STRUCT_0, ALGSTR_0, METRIC_1, TOPMETR, PRE_TOPC, TOPS_1, RLVECT_1, RLSUB_1, RLVECT_2, RLVECT_3, NORMSP_0, NORMSP_1, HAHNBAN, RSSPACE, LOPBAN_1, NFCONT_1, TOPGEN_1, NORMSP_2, DUALSP01, NORMSP_3, DUALSP02, IDEAL_1;
definitions HAHNBAN;
theorems FUNCT_1, ABSVALUE, COMPLEX1, TARSKI, XREAL_0, XXREAL_0, NORMSP_1, FUNCT_2, XBOOLE_0, XREAL_1, RLVECT_1, HAHNBAN, RLSUB_1, RSSPACE, NORMSP_0, ORDINAL1, NAT_1, NDIFF_1, NORMSP_3, ZFMISC_1, XBOOLE_1, TOPGEN_1, DUALSP01, RELAT_1, XCMPLX_1, NORMSP_2, NUMBERS, RLVECT_3, DUALSP02, PRE_TOPC, CARD_1, CARD_2, CARD_3, CARD_4, RLVECT_2, TOPMETR, RAT_1, CARD_5, BORSUK_5, IDEAL_1;
schemes FUNCT_2, NAT_1;
registrations STRUCT_0, XREAL_0, NUMBERS, ORDINAL1, MEMBERED, XXREAL_0, VALUED_0, RLVECT_1, RLVECT_2, FUNCT_2, RELSET_1, NORMSP_3, DUALSP02, FINSET_1, XCMPLX_0, NORMSP_0, NAT_1, NORMSP_1, DUALSP01, XBOOLE_0, SUBSET_1, NORMSP_2, CARD_1, CARD_3, LOPBAN_1, TOPGEN_4, RAT_1;
constructors HIDDEN, REAL_1, REALSET1, RSSPACE3, NFCONT_1, HAHNBAN1, NORMSP_2, PCOMPS_1, RLVECT_2, RLVECT_3, NORMSP_3, TOPS_1, TOPGEN_1, DUALSP02, TOPMETR, IDEAL_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities BINOP_1, STRUCT_0, ALGSTR_0, RLVECT_2, ORDINAL1, NORMSP_3, PCOMPS_1, NORMSP_2;
expansions FUNCT_1, TARSKI, XBOOLE_0, FUNCT_2, STRUCT_0, NORMSP_3, INT_1, PRE_TOPC, CARD_3, DUALSP01;
Lm6:
for X being RealLinearSpace
for v being Element of the carrier of X holds RAT_Sums {v} is countable
Lm13:
for X being RealLinearSpace holds RAT_Sums ({} X) is countable
Th14:
for X being RealLinearSpace
for A being finite Subset of X holds RAT_Sums A is countable
Th16:
for X being RealLinearSpace
for x being sequence of X holds RAT_Sums (rng x) is countable
Th24:
for X being RealNormSpace
for x being sequence of X
for D being Subset of the carrier of (NLin (rng x)) st D = RAT_Sums (rng x) holds
D is dense
Th25:
for X being RealNormSpace
for x being sequence of X
for D being Subset of the carrier of (ClNLin (rng x)) st D = RAT_Sums (rng x) holds
D is dense
Th29:
for X, Y being RealNormSpace
for A being Subset of X
for B being Subset of Y
for L being Lipschitzian LinearOperator of X,Y st L is isomorphism & B = L .: A & A is dense holds
B is dense