environ
vocabularies HIDDEN, RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, INTEGRA1, FDIFF_1, XBOOLE_0, SQUARE_1, ARYTM_3, ORDINAL2, RCOMP_1, PREPOWER, LIMFUNC1, PARTFUN1, TAYLOR_1, SIN_COS9, SUBSET_1, TARSKI, NUMBERS, REAL_1, CARD_1, INTEGRA5, XXREAL_2, ORDINAL4, VALUED_1, XXREAL_1, XXREAL_0, 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, SIN_COS4, SIN_COS9, LIMFUNC1, SEQ_4;
definitions TARSKI, XBOOLE_0;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, XCMPLX_1, INTEGRA5, SIN_COS, TAYLOR_1, VALUED_1, XREAL_0, XBOOLE_0, XXREAL_1, XBOOLE_1, FDIFF_5, FDIFF_7, FDIFF_8, SIN_COS9, PREPOWER, TARSKI, 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, SIN_COS9, PARTFUN2, RFUNCT_1, SIN_COS4, LIMFUNC1, RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, BINOP_2;
requirements HIDDEN, NUMERALS, SUBSET, ARITHM;
equalities SIN_COS, VALUED_1, SQUARE_1, SIN_COS4, LIMFUNC1, XCMPLX_0;
expansions TARSKI;
Lm1:
for Z being open Subset of REAL st 0 in Z holds
(id Z) " {0} = {0}
Lm2:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;