environ
vocabularies HIDDEN, RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, VALUED_1, NAT_1, INTEGRA1, FDIFF_1, SQUARE_1, ARYTM_3, ORDINAL2, PREPOWER, REAL_1, PARTFUN1, TAYLOR_1, CARD_1, ORDINAL4, RCOMP_1, INTEGRA5, XXREAL_0, SIN_COS4, SUBSET_1, XBOOLE_0, TARSKI, NUMBERS, XXREAL_2, SEQ_4, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5, PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, FDIFF_9, SIN_COS4, SEQ_4;
definitions TARSKI, XBOOLE_0;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, TARSKI, XBOOLE_0, INTEGRA5, SIN_COS, VALUED_1, XBOOLE_1, FDIFF_7, FDIFF_8, FDIFF_9, FDIFF_10, SIN_COS9, RELAT_1, FDIFF_2;
schemes ;
registrations NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, RCOMP_1, RELSET_1, MEASURE5, XREAL_0, SQUARE_1, PREPOWER;
constructors HIDDEN, SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER, INTEGRA5, SEQ_4, PARTFUN2, RFUNCT_1, FDIFF_9, SIN_COS4, RELSET_1, INTEGRA1, COMSEQ_2, BINOP_2;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM;
equalities SIN_COS, VALUED_1, SIN_COS4, FDIFF_9, XCMPLX_0;
expansions TARSKI;
Lm1:
for Z being open Subset of REAL st 0 in Z holds
(id Z) " {0} = {0}