environ
vocabularies HIDDEN, FUNCT_1, NUMBERS, SUBSET_1, SUPINF_2, ARYTM_3, CARD_1, RELAT_1, TARSKI, ORDINAL2, XXREAL_0, NAT_1, XXREAL_2, ORDINAL1, XBOOLE_0, ZFMISC_1, FUNCOP_1, MEASURE5, FUNCT_2, SUPINF_1, MCART_1, MEASURE4, REAL_1, PROB_1, MEASURE1, MEASURE7, FUNCT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, XXREAL_3, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NAT_1, PROB_1, XXREAL_2, SUPINF_1, SUPINF_2, MEASURE1, MEASURE4, MEASURE5, RECDEF_1;
definitions TARSKI, MEASURE4, XBOOLE_0, XXREAL_2, VALUED_0;
theorems TARSKI, SUPINF_2, MEASURE1, FUNCT_1, MEASURE5, MEASURE6, ZFMISC_1, FUNCT_2, NAT_1, XBOOLE_0, XBOOLE_1, FUNCOP_1, XXREAL_0, ORDINAL1, XXREAL_2, XXREAL_3, XTUPLE_0;
schemes FUNCT_2, NAT_1, BINOP_2, SUBSET_1, XBOOLE_0, XFAMILY;
registrations XBOOLE_0, SUBSET_1, ORDINAL1, FUNCT_2, NUMBERS, XREAL_0, MEMBERED, MEASURE1, MEASURE4, VALUED_0, XXREAL_2, XXREAL_3, FUNCT_1, RELSET_1, XXREAL_0;
constructors HIDDEN, PARTFUN1, DOMAIN_1, FUNCOP_1, NAT_1, MEASURE4, MEASURE5, RECDEF_1, SUPINF_1, XREAL_0, RELSET_1, XXREAL_2, MEASURE1, PROB_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SUPINF_2;
expansions TARSKI;
REAL in bool REAL
by ZFMISC_1:def 1;
then reconsider G0 = NAT --> REAL as sequence of (bool REAL) by FUNCOP_1:45;
Lm1:
rng G0 = {REAL}
by FUNCOP_1:8;
then Lm2:
REAL c= union (rng G0)
by ZFMISC_1:25;
Lm3:
for n being Element of NAT holds G0 . n is Interval
reconsider D = NAT --> ({} REAL) as sequence of (bool REAL) ;