environ
vocabularies HIDDEN, PRE_TOPC, NORMSP_1, FUNCT_1, ARYTM_1, NAT_1, SUBSET_1, NUMBERS, CARD_1, XXREAL_0, REAL_1, ARYTM_3, RELAT_1, ORDINAL2, SEQ_1, SEQ_2, LOPBAN_1, STRUCT_0, COMPLEX1, VALUED_1, SUPINF_2, XBOOLE_0, ABIAN, INTEGRA1, INTEGRA2, FINSEQ_1, TARSKI, INTEGRA5, INTEGR15, MEASURE7, CARD_3, XXREAL_1, PARTFUN1, SEQ_4, FUNCT_2, RCOMP_1, VALUED_0, XXREAL_2, FCONT_1, MEASURE5, FUNCOP_1, FINSEQ_2, FUNCT_3, ORDINAL4, FCONT_2, ZFMISC_1, INTEGR20;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, FUNCT_1, ORDINAL1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, NAT_1, VALUED_0, COMPLEX1, XXREAL_2, FINSEQ_1, FINSEQ_2, BINOP_1, VALUED_1, SEQ_1, SEQ_2, RFUNCT_1, RVSUM_1, SEQ_4, RCOMP_1, ABIAN, MEASURE5, INTEGRA1, INTEGRA2, INTEGRA3, INTEGRA5, STRUCT_0, PRE_TOPC, RLVECT_1, VFUNCT_1, NORMSP_0, NORMSP_1, LOPBAN_1, BINOM, INTEGR18, NFCONT_3;
definitions ;
theorems ABSVALUE, RLVECT_1, XCMPLX_1, SEQ_2, PARTFUN1, FUNCT_1, NAT_1, FUNCT_2, NORMSP_1, XREAL_1, RSSPACE3, LOPBAN_1, XXREAL_0, XREAL_0, ORDINAL1, RELAT_1, SEQ_4, VFUNCT_1, XBOOLE_0, FUNCOP_1, FINSEQ_1, XXREAL_1, RVSUM_1, VALUED_1, XBOOLE_1, INTEGRA4, INTEGRA3, INTEGRA1, INT_1, INTEGR18, FINSEQ_4, FINSEQ_2, FINSEQ_3, FINSEQ_5, MEASURE5, VALUED_0, XXREAL_2, ZFMISC_1, RFUNCT_2, BINOM, TARSKI;
schemes NAT_1, FUNCT_2, FINSEQ_1, BINOP_1, SUBSET_1;
registrations STRUCT_0, NAT_1, VALUED_1, NORMSP_0, NUMBERS, XBOOLE_0, FUNCT_2, XREAL_0, MEMBERED, RELAT_1, RELSET_1, INTEGRA1, ORDINAL1, NFCONT_3, XXREAL_2, RLVECT_1, VALUED_0, FINSEQ_1, FINSET_1, MEASURE5, ABIAN, SEQM_3, INT_1, CARD_1, SUBSET_1;
constructors HIDDEN, ABIAN, SEQ_2, RSSPACE3, RELSET_1, SEQ_4, VFUNCT_1, NEWTON, INTEGRA3, INTEGR18, RVSUM_1, COMSEQ_2, BINOM, ORDEQ_01, RFUNCT_1, NDIFF_5;
requirements HIDDEN, SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities RCOMP_1, ALGSTR_0, NORMSP_0, FINSEQ_1, INTEGRA1, INTEGRA3, INTEGR18, XCMPLX_0, BINOP_1;
expansions RCOMP_1, ABIAN, FINSEQ_1, NFCONT_3, INTEGR18, NORMSP_1, TARSKI;
Lm1:
for X, Y, Z being non empty set
for f being PartFunc of X,Y st Z c= dom f holds
f | Z is Function of Z,Y
Lm2:
for Y being RealNormSpace
for xseq, yseq being FinSequence of Y st len xseq = (len yseq) + 1 & xseq | (len yseq) = yseq holds
ex v being Point of Y st
( v = xseq /. (len xseq) & Sum xseq = (Sum yseq) + v )
theorem Th14:
for
n being
Nat ex
k being
Nat st
(
n = 2
* k or
n = (2 * k) + 1 )