environ
vocabularies HIDDEN, NUMBERS, SIN_COS4, PARTFUN1, SIN_COS, ORDINAL4, REAL_1, RCOMP_1, SUBSET_1, FUNCT_1, CARD_1, FDIFF_1, ARYTM_3, SQUARE_1, ARYTM_1, PREPOWER, NEWTON, TARSKI, RELAT_1, VALUED_1, XBOOLE_0, LIMFUNC1, TAYLOR_1, XXREAL_0, NAT_1;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, RELSET_1, FUNCT_1, PARTFUN1, PARTFUN2, RCOMP_1, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, XCMPLX_0, XREAL_0, 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, FDIFF_8, VALUED_1, XXREAL_1;
schemes ;
registrations RELSET_1, XREAL_0, MEMBERED, RCOMP_1, INT_1, XXREAL_0, NUMBERS, ORDINAL1, VALUED_0, SQUARE_1, PREPOWER, NEWTON;
constructors HIDDEN, REAL_1, PARTFUN1, PARTFUN2, NAT_1, LIMFUNC1, RCOMP_1, TAYLOR_1, SIN_COS, FDIFF_1, RFUNCT_1, SQUARE_1, PREPOWER, 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;