environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, FINSEQ_1, RELAT_1, TREES_1, XBOOLE_0, ARYTM_3, XXREAL_0, ORDINAL4, CARD_1, FUNCT_1, TARSKI, TREES_2, TREES_9, ORDINAL1, NAT_1, FINSET_1, QC_LANG1, ZF_LANG, CLASSES2, TREES_4, QC_LANG4;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, NAT_1, RELAT_1, FUNCT_1, FUNCT_2, BINOP_1, FINSET_1, FINSEQ_1, FINSEQ_4, TREES_1, TREES_2, TREES_4, TREES_9, QC_LANG1, QC_LANG2, XXREAL_0;
definitions TARSKI, XBOOLE_0, TREES_2, TREES_4;
theorems TARSKI, NAT_1, RELAT_1, FUNCT_1, FINSEQ_1, TREES_1, TREES_2, TREES_9, GRFUNC_1, QC_LANG1, QC_LANG2, XBOOLE_0, FINSEQ_6, XREAL_1, XXREAL_0, ORDINAL1;
schemes NAT_1, TREES_2, FINSEQ_1, TREES_9;
registrations ORDINAL1, XREAL_0, NAT_1, FINSEQ_1, TREES_2, TREES_A, TREES_9, CARD_1, RELAT_1;
constructors HIDDEN, BINOP_1, XXREAL_0, XREAL_0, NAT_1, FINSEQ_4, TREES_4, TREES_9, QC_LANG2, RELSET_1, XTUPLE_0, NUMBERS;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities XBOOLE_0, TREES_2;
expansions TARSKI, XBOOLE_0;
Lm1:
for x, y being set holds dom <*x,y*> = Seg 2