environ
vocabularies HIDDEN, NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, NAT_1, FUNCT_1, RELAT_1, XBOOLE_0, ARYTM_1, VALUED_1, TARSKI, XXREAL_0, PREPOWER, ORDINAL4, CARD_1, NEWTON, ARYTM_3, FDIFF_1, SIN_COS, ABIAN, SQUARE_1, REALSET1, TAYLOR_1, TAYLOR_2, XXREAL_1, COMPLEX1, FUNCOP_1, FUNCT_7;
notations HIDDEN, SUBSET_1, FUNCT_1, PARTFUN1, RCOMP_1, XXREAL_0, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, FUNCT_2, XREAL_0, FUNCOP_1, REAL_1, NAT_1, NAT_D, VALUED_1, TAYLOR_2, FDIFF_1, SEQFUNC, NEWTON, SIN_COS, TAYLOR_1, ABIAN, XBOOLE_0, TARSKI, PREPOWER, RFUNCT_1, SQUARE_1, RELSET_1;
definitions TAYLOR_1, TARSKI, XBOOLE_0;
theorems RFUNCT_1, XBOOLE_0, NEWTON, XCMPLX_1, FUNCT_1, XBOOLE_1, ABSVALUE, PARTFUN1, RELAT_1, RCOMP_1, SIN_COS, NAT_1, FDIFF_1, FDIFF_2, TAYLOR_1, SIN_COS2, XREAL_1, ABIAN, XXREAL_0, TAYLOR_2, INT_1, WSIERP_1, FUNCT_2, TARSKI, XCMPLX_0, VALUED_1, PREPOWER, ZFMISC_1, FDIFF_7, FDIFF_8, FDIFF_4, FUNCOP_1, XREAL_0, ORDINAL1;
schemes NAT_1;
registrations RELSET_1, NUMBERS, NAT_1, MEMBERED, VALUED_0, RCOMP_1, FUNCT_1, INT_1, ORDINAL1, FUNCT_2, XREAL_0, NEWTON, PREPOWER, SQUARE_1;
constructors HIDDEN, REAL_1, NAT_1, RCOMP_1, LIMFUNC1, TAYLOR_2, FDIFF_1, SIN_COS, ABIAN, TAYLOR_1, RFUNCT_1, SQUARE_1, PREPOWER, BINARITH, PARTFUN2, VALUED_1, BINOP_2, NAT_D, SEQFUNC, RELSET_1, NEWTON, NUMBERS;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities VALUED_1, SQUARE_1, XBOOLE_0;
expansions TAYLOR_1, TARSKI;
Lm1:
for n, m being Element of NAT st n > 1 holds
((m !) / (n !)) * n = (m !) / ((n -' 1) !)
Lm2:
#Z 1 = id REAL
Lm3:
for Z being open Subset of REAL
for f being PartFunc of REAL,REAL st f is_differentiable_on Z holds
(f `| Z) `| Z = (diff (f,Z)) . 2
Lm4:
for f being PartFunc of REAL,REAL holds f / f = ((dom f) \ (f " {0})) --> 1
Lm5:
for f being PartFunc of REAL,REAL holds (f (#) (f (#) f)) " {0} = f " {0}