environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, AFINSQ_1, NAT_1, TARSKI, RELAT_1, PRE_POLY, XXREAL_0, NEWTON, SETFAM_1, XBOOLE_0, CARD_1, ARYTM_3, ORDINAL4, MODAL_1, FLANG_3;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, SETFAM_1, XXREAL_0, AFINSQ_1, FLANG_1, FLANG_2;
definitions TARSKI;
theorems NAT_1, TARSKI, XBOOLE_0, XBOOLE_1, XREAL_1, ZFMISC_1, FLANG_1, XXREAL_0, FLANG_2;
schemes CARD_FIL, DOMAIN_1, NAT_1;
registrations SUBSET_1, NAT_1, ORDINAL1, AFINSQ_1, XREAL_0, XBOOLE_0;
constructors HIDDEN, NAT_1, XREAL_0, FLANG_1, FLANG_2;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities ;
expansions TARSKI;
:: Definition of |^.. n