environ
vocabularies HIDDEN, REAL_1, XBOOLE_0, SUBSET_1, NUMBERS, INTEGRA1, PARTFUN1, RCOMP_1, RELAT_1, ARYTM_1, SIN_COS, JGRAPH_2, CARD_1, FDIFF_1, FUNCT_1, ARYTM_3, VALUED_1, SEQ_4, ORDINAL2, INTEGRA5, XXREAL_2, TARSKI, PREPOWER, NEWTON, REALSET1, XXREAL_0, XXREAL_1, SQUARE_1, ORDINAL4, TAYLOR_1, SIN_COS4, INTEGRA9, MEASURE5;
notations HIDDEN, FUNCT_1, SIN_COS, TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1, SEQ_4, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, RELSET_1, PARTFUN1, RFUNCT_1, RCOMP_1, MEASURE5, INTEGRA1, FCONT_1, FDIFF_9, SQUARE_1, INTEGRA5, PARTFUN2, NEWTON, PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2;
definitions ;
theorems PARTFUN1, INTEGRA1, RFUNCT_1, FUNCT_1, FDIFF_1, INTEGRA2, FUNCT_2, XBOOLE_0, XBOOLE_1, SQUARE_1, XCMPLX_1, INTEGRA5, INTEGRA8, INTEGRA6, SIN_COS, XREAL_1, FDIFF_4, TAYLOR_1, FDIFF_6, VALUED_1, FCONT_1, RELAT_1, FDIFF_2, FDIFF_5, FDIFF_8, FDIFF_9, PREPOWER, XREAL_0;
schemes ;
registrations VALUED_1, NAT_1, XBOOLE_0, NUMBERS, MEMBERED, VALUED_0, RCOMP_1, INT_1, ORDINAL1, FUNCT_2, RELSET_1, FCONT_1, FCONT_3, MEASURE5, XREAL_0, PREPOWER, SIN_COS, SQUARE_1, NEWTON;
constructors HIDDEN, SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER, INTEGRA5, PARTFUN2, LIMFUNC1, SEQ_4, RFUNCT_1, FDIFF_9, RELSET_1, SEQ_2, NEWTON, INTEGRA1, COMSEQ_2, BINOP_2, NUMBERS;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM;
equalities SIN_COS, INTEGRA5, VALUED_1, SUBSET_1, FDIFF_9;
expansions INTEGRA5;
Lm1:
dom (- (exp_R * (AffineMap ((- 1),0)))) = [#] REAL
by FUNCT_2:def 1;
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm2:
for x being Real holds
( - sin is_differentiable_in x & diff ((- sin),x) = - (cos . x) )
theorem Th31:
for
f,
g being
PartFunc of
REAL,
REAL for
A being non
empty closed_interval Subset of
REAL st
(f (#) f) || A is
total &
(f (#) g) || A is
total &
(g (#) g) || A is
total &
((f (#) f) || A) | A is
bounded &
((f (#) g) || A) | A is
bounded &
((g (#) g) || A) | A is
bounded &
f (#) f is_integrable_on A &
f (#) g is_integrable_on A &
g (#) g is_integrable_on A holds
|||((f + g),(f + g),A)||| = (|||(f,f,A)||| + (2 * |||(f,g,A)|||)) + |||(g,g,A)|||