environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, CQC_LANG, QC_LANG1, XBOOLE_0, VALUAT_1, FINSEQ_1, HENMODEL, CQC_THE1, XBOOLEAN, BVFUNC_2, FUNCT_1, ORDINAL4, CALCUL_1, ARYTM_3, RELAT_1, CARD_1, XXREAL_0, TARSKI, ZF_MODEL, CQC_SIM1, REALSET1, SUBSTUT1, SUBSTUT2, ZF_LANG, ARYTM_1, CARD_3, ZFMISC_1, FINSET_1, MCART_1, GOEDELCP, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, XCMPLX_0, XXREAL_0, ORDINAL1, CARD_1, CARD_3, FINSEQ_1, FUNCT_1, NAT_1, QC_LANG1, QC_LANG2, QC_LANG3, NUMBERS, CQC_LANG, RELAT_1, FINSET_1, VALUAT_1, RELSET_1, FUNCT_2, CQC_SIM1, DOMAIN_1, XTUPLE_0, XFAMILY, MCART_1, SUBSTUT1, SUBLEMMA, SUBSTUT2, CALCUL_1, HENMODEL;
definitions TARSKI, XBOOLE_0;
theorems TARSKI, FUNCT_1, MCART_1, XBOOLE_0, XBOOLE_1, CQC_LANG, QC_LANG1, ZFMISC_1, QC_LANG3, QC_LANG2, HENMODEL, CALCUL_1, SUBLEMMA, NAT_1, FINSEQ_1, VALUAT_1, FUNCT_2, SUBSTUT2, CQC_SIM1, CARD_4, CALCUL_2, SUPINF_2, XREAL_1, XXREAL_0, ORDINAL1;
schemes XBOOLE_0, NAT_1, FUNCT_1, SUBSTUT2, RECDEF_1;
registrations SUBSET_1, RELAT_1, ORDINAL1, XXREAL_0, XREAL_0, CQC_LANG, HENMODEL, FINSEQ_1, FINSET_1, CARD_3, RELSET_1, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, XXREAL_0, NAT_1, NAT_D, FINSEQ_2, QC_LANG3, CQC_SIM1, SUBSTUT2, CALCUL_1, HENMODEL, CARD_3, RELSET_1, XTUPLE_0, XFAMILY;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities XBOOLE_0, ORDINAL1, CARD_1;
expansions TARSKI, XBOOLE_0;
Lm1:
for A being non empty set st A is countable holds
ex f being Function st
( dom f = NAT & A = rng f )