environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, REAL_1, COMSEQ_1, COMPLEX1, RELAT_1, ARYTM_1, ARYTM_3, CARD_1, XXREAL_0, FUNCT_1, XBOOLE_0, PARTFUN1, VALUED_0, VALUED_1, XXREAL_2, FUNCOP_1, SEQ_2, ORDINAL2, XCMPLX_0, PBOOLE, TARSKI, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, COMPLEX1, RELAT_1, REAL_1, FUNCT_1, PBOOLE, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, VALUED_0, VALUED_1, NAT_1, COMSEQ_1, XXREAL_0;
definitions RELAT_1, FUNCT_1, PARTFUN1;
theorems COMSEQ_1, COMPLEX1, NAT_1, FUNCT_2, XREAL_0, XCMPLX_0, XCMPLX_1, FUNCOP_1, XREAL_1, XXREAL_0, VALUED_1, PARTFUN1, VALUED_0, ORDINAL1, NUMBERS;
schemes NAT_1, FUNCT_1;
registrations XBOOLE_0, ORDINAL1, RELSET_1, FUNCT_2, NUMBERS, XXREAL_0, XREAL_0, MEMBERED, VALUED_1, VALUED_0, XCMPLX_0, NAT_1;
constructors HIDDEN, PARTFUN1, FUNCOP_1, REAL_1, SQUARE_1, NAT_1, COMPLEX1, VALUED_1, RELSET_1, PBOOLE, NUMBERS;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities VALUED_1;
expansions ;
reconsider sc = NAT --> 0c as Complex_Sequence ;
reconsider zz = 0 as Nat ;