environ
vocabularies HIDDEN, NUMBERS, REAL_1, RCOMP_1, SUBSET_1, PARTFUN1, RELAT_1, SIN_COS, FUNCT_1, CARD_1, XBOOLE_0, ORDINAL4, TARSKI, ARYTM_3, PREPOWER, NEWTON, ARYTM_1, FDIFF_1, SQUARE_1, LIMFUNC1, TAYLOR_1, XXREAL_0, VALUED_1, NAT_1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, PARTFUN2, XCMPLX_0, XREAL_0, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1, NAT_1, NEWTON, VALUED_1, FDIFF_1, PREPOWER, LIMFUNC1;
definitions ;
theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, NAT_1, FDIFF_1, SQUARE_1, FDIFF_7, FDIFF_4, RFUNCT_1, PREPOWER, FDIFF_5, FUNCT_1, NEWTON, SIN_COS, RELAT_1, XBOOLE_0, VALUED_1, XXREAL_1;
schemes ;
registrations ORDINAL1, RELSET_1, NUMBERS, XXREAL_0, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0, SQUARE_1, PREPOWER, NEWTON;
constructors HIDDEN, PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, LIMFUNC1, FDIFF_1, PREPOWER, SIN_COS, TAYLOR_1, VALUED_1, RELSET_1, NEWTON;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities SQUARE_1, LIMFUNC1, XCMPLX_0, SIN_COS, VALUED_1;
expansions ;
Lm1:
right_open_halfline 0 = { g where g is Real : 0 < g }
by XXREAL_1:230;