environ
vocabularies HIDDEN, RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, INTEGRA1, FDIFF_1, XBOOLE_0, SQUARE_1, ARYTM_3, ORDINAL2, RCOMP_1, PREPOWER, NEWTON, NUMBERS, REAL_1, SUBSET_1, XXREAL_0, XXREAL_1, PARTFUN1, TAYLOR_1, SIN_COS6, SIN_COS9, LIMFUNC1, TARSKI, VALUED_1, CARD_1, ORDINAL4, INTEGRA5, NAT_1, XXREAL_2, SEQ_4, MEASURE5;
notations HIDDEN, TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1, XCMPLX_0, NAT_1, XXREAL_0, XREAL_0, REAL_1, RELSET_1, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, MEASURE6, INTEGRA1, FCONT_1, SQUARE_1, INTEGRA5, TAYLOR_1, FDIFF_1, SEQ_2, SEQ_4, SIN_COS6, SIN_COS9, NEWTON, LIMFUNC1, PREPOWER;
definitions TARSKI;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, XCMPLX_1, RELAT_1, INTEGRA5, SIN_COS, FDIFF_4, TAYLOR_1, VALUED_1, FCONT_1, SIN_COS6, XXREAL_1, XBOOLE_1, PREPOWER, FDIFF_2, XREAL_1, NAT_1, FDIFF_5, FDIFF_7, FDIFF_8, SIN_COS9, XBOOLE_0, XREAL_0;
schemes ;
registrations NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, ORDINAL1, FUNCT_2, RCOMP_1, RELSET_1, XREAL_0, NEWTON, SQUARE_1, MEASURE5, PREPOWER;
constructors HIDDEN, SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, MEASURE6, BINOP_2, SQUARE_1, PREPOWER, INTEGRA5, SEQ_4, XXREAL_3, XBOOLE_0, SEQ_2, LIMFUNC1, NAT_1, POWER, RELSET_1, TARSKI, SIN_COS9, PARTFUN1, PARTFUN2, FUNCT_1, RCOMP_1, RELAT_1, SIN_COS6, RFUNCT_1, VALUED_1, FDIFF_9, NEWTON, INTEGRA1, COMSEQ_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities SIN_COS, VALUED_1, SQUARE_1, LIMFUNC1, XCMPLX_0;
expansions TARSKI;
Lm1:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;