:: INTEGRA7 semantic presentation

REAL is non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V100() set
NAT is V50() V51() V52() V53() V54() V55() V56() bounded_below Element of K6(REAL)
K6(REAL) is set
K7(REAL,REAL) is V40() V41() V42() set
K6(K7(REAL,REAL)) is set
{} is empty V50() V51() V52() V53() V54() V55() V56() bounded_below V100() set
1 is non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below Element of NAT
{{},1} is non empty set
COMPLEX is non empty V50() V56() V57() set
omega is V50() V51() V52() V53() V54() V55() V56() bounded_below set
K6(omega) is set
K6(NAT) is set
ExtREAL is non empty V51() V100() set
K7(NAT,REAL) is V40() V41() V42() set
K6(K7(NAT,REAL)) is set
RAT is non empty V50() V51() V52() V53() V56() V57() set
INT is non empty V50() V51() V52() V53() V54() V56() V57() set
K7(COMPLEX,COMPLEX) is V40() set
K6(K7(COMPLEX,COMPLEX)) is set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is V40() set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is set
K7(K7(REAL,REAL),REAL) is V40() V41() V42() set
K6(K7(K7(REAL,REAL),REAL)) is set
K7(RAT,RAT) is V17( RAT ) V40() V41() V42() set
K6(K7(RAT,RAT)) is set
K7(K7(RAT,RAT),RAT) is V17( RAT ) V40() V41() V42() set
K6(K7(K7(RAT,RAT),RAT)) is set
K7(INT,INT) is V17( RAT ) V17( INT ) V40() V41() V42() set
K6(K7(INT,INT)) is set
K7(K7(INT,INT),INT) is V17( RAT ) V17( INT ) V40() V41() V42() set
K6(K7(K7(INT,INT),INT)) is set
K7(NAT,NAT) is V17( RAT ) V17( INT ) V40() V41() V42() V43() set
K7(K7(NAT,NAT),NAT) is V17( RAT ) V17( INT ) V40() V41() V42() V43() set
K6(K7(K7(NAT,NAT),NAT)) is set
K7(NAT,COMPLEX) is V40() set
K6(K7(NAT,COMPLEX)) is set
PFuncs (REAL,REAL) is set
K7(NAT,(PFuncs (REAL,REAL))) is set
K6(K7(NAT,(PFuncs (REAL,REAL)))) is set
K7(COMPLEX,REAL) is V40() V41() V42() set
K6(K7(COMPLEX,REAL)) is set
0 is empty natural V11() real ext-real V50() V51() V52() V53() V54() V55() V56() V89() V90() bounded_below V100() Element of NAT
{0} is non empty V50() V51() V52() V53() V54() V55() left_end bounded_below set
2 is non empty natural V11() real ext-real positive V50() V51() V52() V53() V54() V55() V89() V90() left_end bounded_below Element of NAT
sin is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
dom sin is V50() V51() V52() Element of K6(REAL)
cos is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
dom cos is V50() V51() V52() Element of K6(REAL)
exp_R is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
dom exp_R is V50() V51() V52() Element of K6(REAL)
[#] REAL is V50() V51() V52() closed open Element of K6(REAL)
rng exp_R is V50() V51() V52() Element of K6(REAL)
K265(0) is V50() V51() V52() open Element of K6(REAL)
a is V11() real ext-real set
b is non empty set
K7(b,REAL) is V40() V41() V42() set
K6(K7(b,REAL)) is set
H is non empty V13() V16(b) V17( REAL ) V18() total V27(b, REAL ) V40() V41() V42() Element of K6(K7(b,REAL))
rng H is V50() V51() V52() Element of K6(REAL)
rseq is non empty V13() V16(b) V17( REAL ) V18() total V27(b, REAL ) V40() V41() V42() Element of K6(K7(b,REAL))
rng rseq is V50() V51() V52() Element of K6(REAL)
upper_bound (rng H) is V11() real ext-real Element of REAL
upper_bound (rng rseq) is V11() real ext-real Element of REAL
(upper_bound (rng H)) - (upper_bound (rng rseq)) is V11() real ext-real Element of REAL
- (upper_bound (rng rseq)) is V11() real ext-real set
(upper_bound (rng H)) + (- (upper_bound (rng rseq))) is V11() real ext-real set
(upper_bound (rng rseq)) - (upper_bound (rng H)) is V11() real ext-real Element of REAL
- (upper_bound (rng H)) is V11() real ext-real set
(upper_bound (rng rseq)) + (- (upper_bound (rng H))) is V11() real ext-real set
dom H is Element of K6(b)
K6(b) is set
(upper_bound (rng H)) + a is V11() real ext-real Element of REAL
AB is V11() real ext-real set
dom rseq is Element of K6(b)
T is Element of b
rseq . T is V11() real ext-real Element of REAL
H . T is V11() real ext-real Element of REAL
(H . T) - (rseq . T) is V11() real ext-real Element of REAL
- (rseq . T) is V11() real ext-real set
(H . T) + (- (rseq . T)) is V11() real ext-real set
abs ((H . T) - (rseq . T)) is V11() real ext-real Element of REAL
(rseq . T) - (H . T) is V11() real ext-real Element of REAL
- (H . T) is V11() real ext-real set
(rseq . T) + (- (H . T)) is V11() real ext-real set
abs ((rseq . T) - (H . T)) is V11() real ext-real Element of REAL
a + (H . T) is V11() real ext-real Element of REAL
a + (upper_bound (rng H)) is V11() real ext-real Element of REAL
dom rseq is Element of K6(b)
(upper_bound (rng rseq)) + a is V11() real ext-real Element of REAL
AB is V11() real ext-real set
T is Element of b
H . T is V11() real ext-real Element of REAL
rseq . T is V11() real ext-real Element of REAL
a + (rseq . T) is V11() real ext-real Element of REAL
a + (upper_bound (rng rseq)) is V11() real ext-real Element of REAL
(H . T) - (rseq . T) is V11() real ext-real Element of REAL
- (rseq . T) is V11() real ext-real set
(H . T) + (- (rseq . T)) is V11() real ext-real set
abs ((H . T) - (rseq . T)) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is non empty set
K7(b,REAL) is V40() V41() V42() set
K6(K7(b,REAL)) is set
H is non empty V13() V16(b) V17( REAL ) V18() total V27(b, REAL ) V40() V41() V42() Element of K6(K7(b,REAL))
rng H is V50() V51() V52() Element of K6(REAL)
rseq is non empty V13() V16(b) V17( REAL ) V18() total V27(b, REAL ) V40() V41() V42() Element of K6(K7(b,REAL))
rng rseq is V50() V51() V52() Element of K6(REAL)
lower_bound (rng H) is V11() real ext-real Element of REAL
lower_bound (rng rseq) is V11() real ext-real Element of REAL
(lower_bound (rng H)) - (lower_bound (rng rseq)) is V11() real ext-real Element of REAL
- (lower_bound (rng rseq)) is V11() real ext-real set
(lower_bound (rng H)) + (- (lower_bound (rng rseq))) is V11() real ext-real set
(lower_bound (rng rseq)) - (lower_bound (rng H)) is V11() real ext-real Element of REAL
- (lower_bound (rng H)) is V11() real ext-real set
(lower_bound (rng rseq)) + (- (lower_bound (rng H))) is V11() real ext-real set
dom H is Element of K6(b)
K6(b) is set
(lower_bound (rng H)) - a is V11() real ext-real Element of REAL
- a is V11() real ext-real set
(lower_bound (rng H)) + (- a) is V11() real ext-real set
AB is V11() real ext-real set
dom rseq is Element of K6(b)
T is Element of b
rseq . T is V11() real ext-real Element of REAL
H . T is V11() real ext-real Element of REAL
(H . T) - a is V11() real ext-real Element of REAL
(H . T) + (- a) is V11() real ext-real set
(H . T) - (rseq . T) is V11() real ext-real Element of REAL
- (rseq . T) is V11() real ext-real set
(H . T) + (- (rseq . T)) is V11() real ext-real set
abs ((H . T) - (rseq . T)) is V11() real ext-real Element of REAL
dom rseq is Element of K6(b)
(lower_bound (rng rseq)) - a is V11() real ext-real Element of REAL
(lower_bound (rng rseq)) + (- a) is V11() real ext-real set
AB is V11() real ext-real set
T is Element of b
H . T is V11() real ext-real Element of REAL
rseq . T is V11() real ext-real Element of REAL
(H . T) - (rseq . T) is V11() real ext-real Element of REAL
- (rseq . T) is V11() real ext-real set
(H . T) + (- (rseq . T)) is V11() real ext-real set
abs ((H . T) - (rseq . T)) is V11() real ext-real Element of REAL
(rseq . T) - (H . T) is V11() real ext-real Element of REAL
- (H . T) is V11() real ext-real set
(rseq . T) + (- (H . T)) is V11() real ext-real set
abs ((rseq . T) - (H . T)) is V11() real ext-real Element of REAL
(rseq . T) - a is V11() real ext-real Element of REAL
(rseq . T) + (- a) is V11() real ext-real set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is set
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(b | a) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V11() real ext-real Element of REAL
dom (b | a) is V50() V51() V52() Element of K6(REAL)
(b | a) . H is V11() real ext-real Element of REAL
rseq is V50() V51() V52() open Neighbourhood of H
b . H is V11() real ext-real Element of REAL
dom b is V50() V51() V52() Element of K6(REAL)
(dom b) /\ a is V50() V51() V52() Element of K6(REAL)
AB is V13() V16( REAL ) V17( REAL ) V18() linear V40() V41() V42() Element of K6(K7(REAL,REAL))
T is V13() V16( REAL ) V17( REAL ) V18() RestFunc-like V40() V41() V42() Element of K6(K7(REAL,REAL))
AB is V13() V16( REAL ) V17( REAL ) V18() linear V40() V41() V42() Element of K6(K7(REAL,REAL))
T is V13() V16( REAL ) V17( REAL ) V18() RestFunc-like V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 is V11() real ext-real Element of REAL
b . L1 is V11() real ext-real Element of REAL
(b . L1) - (b . H) is V11() real ext-real Element of REAL
- (b . H) is V11() real ext-real set
(b . L1) + (- (b . H)) is V11() real ext-real set
L1 - H is V11() real ext-real Element of REAL
- H is V11() real ext-real set
L1 + (- H) is V11() real ext-real set
AB . (L1 - H) is V11() real ext-real Element of REAL
T . (L1 - H) is V11() real ext-real Element of REAL
(AB . (L1 - H)) + (T . (L1 - H)) is V11() real ext-real Element of REAL
(b | a) . L1 is V11() real ext-real Element of REAL
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V11() real ext-real Element of REAL
(b | a) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (b | a) is V50() V51() V52() Element of K6(REAL)
dom b is V50() V51() V52() Element of K6(REAL)
(dom b) /\ a is V50() V51() V52() Element of K6(REAL)
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b + H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b - H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
- H is V13() V16( REAL ) V18() V40() V41() V42() set
- 1 is V11() real ext-real V89() set
(- 1) (#) H is V13() V16( REAL ) V18() V40() V41() V42() set
b + (- H) is V13() V16( REAL ) V18() V40() V41() V42() set
b (#) H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V50() V51() V52() Element of K6(REAL)
dom b is V50() V51() V52() Element of K6(REAL)
dom H is V50() V51() V52() Element of K6(REAL)
AB is V50() V51() V52() open Element of K6(REAL)
(dom b) /\ (dom H) is V50() V51() V52() Element of K6(REAL)
dom (b (#) H) is V50() V51() V52() Element of K6(REAL)
dom (b + H) is V50() V51() V52() Element of K6(REAL)
dom (b - H) is V50() V51() V52() Element of K6(REAL)
a is V11() real ext-real set
b is set
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a (#) H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB is V50() V51() V52() Element of K6(REAL)
dom H is V50() V51() V52() Element of K6(REAL)
T is V50() V51() V52() open Element of K6(REAL)
dom (a (#) H) is V50() V51() V52() Element of K6(REAL)
rseq is V11() real ext-real Element of REAL
rseq (#) H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H / b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V50() V51() V52() Element of K6(REAL)
AB is V50() V51() V52() open Element of K6(REAL)
T is V11() real ext-real Element of REAL
b . T is V11() real ext-real Element of REAL
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b ^ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V50() V51() V52() Element of K6(REAL)
rseq is V50() V51() V52() open Element of K6(REAL)
AB is V11() real ext-real Element of REAL
b . AB is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq `| H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq `| H) | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq . b is V11() real ext-real Element of REAL
integral ((rseq `| H),a,b) is V11() real ext-real Element of REAL
rseq . a is V11() real ext-real Element of REAL
(integral ((rseq `| H),a,b)) + (rseq . a) is V11() real ext-real Element of REAL
integral ((rseq `| H),['a,b']) is V11() real ext-real Element of REAL
(rseq `| H) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V40() V41() V42() set
K6(K7(['a,b'],REAL)) is set
integral ((rseq `| H) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((rseq `| H) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((rseq `| H) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (upper_sum_set ((rseq `| H) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((rseq `| H) || ['a,b']))) is V11() real ext-real Element of REAL
upper_bound ['a,b'] is V11() real ext-real Element of REAL
rseq . (upper_bound ['a,b']) is V11() real ext-real Element of REAL
lower_bound ['a,b'] is V11() real ext-real Element of REAL
rseq . (lower_bound ['a,b']) is V11() real ext-real Element of REAL
(rseq . (upper_bound ['a,b'])) - (rseq . (lower_bound ['a,b'])) is V11() real ext-real Element of REAL
- (rseq . (lower_bound ['a,b'])) is V11() real ext-real set
(rseq . (upper_bound ['a,b'])) + (- (rseq . (lower_bound ['a,b']))) is V11() real ext-real set
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
lower_bound [.a,b.] is V11() real ext-real Element of REAL
upper_bound [.a,b.] is V11() real ext-real Element of REAL
[.(lower_bound [.a,b.]),(upper_bound [.a,b.]).] is V50() V51() V52() closed V100() Element of K6(REAL)
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is set
rseq is set
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is set
rseq is set
AB is set
T is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(a,H) is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom b is V50() V51() V52() Element of K6(REAL)
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(a,H) is set
H | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b + rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b - rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
- rseq is V13() V16( REAL ) V18() V40() V41() V42() set
- 1 is V11() real ext-real V89() set
(- 1) (#) rseq is V13() V16( REAL ) V18() V40() V41() V42() set
b + (- rseq) is V13() V16( REAL ) V18() V40() V41() V42() set
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H + AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H - AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
- AB is V13() V16( REAL ) V18() V40() V41() V42() set
(- 1) (#) AB is V13() V16( REAL ) V18() V40() V41() V42() set
H + (- AB) is V13() V16( REAL ) V18() V40() V41() V42() set
rseq `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (AB | a) is V50() V51() V52() Element of K6(REAL)
dom AB is V50() V51() V52() Element of K6(REAL)
(dom AB) /\ a is V50() V51() V52() Element of K6(REAL)
b `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (H | a) is V50() V51() V52() Element of K6(REAL)
dom H is V50() V51() V52() Element of K6(REAL)
(dom H) /\ a is V50() V51() V52() Element of K6(REAL)
(dom H) /\ (dom AB) is V50() V51() V52() Element of K6(REAL)
dom (H + AB) is V50() V51() V52() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(b + rseq) `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((b + rseq) `| a) is V50() V51() V52() Element of K6(REAL)
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq `| a) . T is V11() real ext-real Element of REAL
diff (rseq,T) is V11() real ext-real Element of REAL
AB . T is V11() real ext-real Element of REAL
(b `| a) . T is V11() real ext-real Element of REAL
diff (b,T) is V11() real ext-real Element of REAL
H . T is V11() real ext-real Element of REAL
rseq | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((b + rseq) `| a) . T is V11() real ext-real Element of REAL
diff ((b + rseq),T) is V11() real ext-real Element of REAL
(diff (b,T)) + (diff (rseq,T)) is V11() real ext-real Element of REAL
(H + AB) . T is V11() real ext-real Element of REAL
(H + AB) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((H + AB) | a) . T is V11() real ext-real Element of REAL
dom (H - AB) is V50() V51() V52() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(b - rseq) `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((b - rseq) `| a) is V50() V51() V52() Element of K6(REAL)
(rseq `| a) . T is V11() real ext-real Element of REAL
diff (rseq,T) is V11() real ext-real Element of REAL
AB . T is V11() real ext-real Element of REAL
(b `| a) . T is V11() real ext-real Element of REAL
diff (b,T) is V11() real ext-real Element of REAL
H . T is V11() real ext-real Element of REAL
((b - rseq) `| a) . T is V11() real ext-real Element of REAL
diff ((b - rseq),T) is V11() real ext-real Element of REAL
(diff (b,T)) - (diff (rseq,T)) is V11() real ext-real Element of REAL
- (diff (rseq,T)) is V11() real ext-real set
(diff (b,T)) + (- (diff (rseq,T))) is V11() real ext-real set
(H - AB) . T is V11() real ext-real Element of REAL
(H - AB) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((H - AB) | a) . T is V11() real ext-real Element of REAL
dom ((H + AB) | a) is V50() V51() V52() Element of K6(REAL)
dom ((H - AB) | a) is V50() V51() V52() Element of K6(REAL)
a is V11() real ext-real set
b is set
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a (#) H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a (#) rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H `| b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq | b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (rseq | b) is V50() V51() V52() Element of K6(REAL)
dom rseq is V50() V51() V52() Element of K6(REAL)
(dom rseq) /\ b is V50() V51() V52() Element of K6(REAL)
dom (a (#) rseq) is V50() V51() V52() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(a (#) H) `| b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((a (#) H) `| b) is V50() V51() V52() Element of K6(REAL)
H | b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((a (#) H) `| b) . T is V11() real ext-real Element of REAL
diff ((a (#) H),T) is V11() real ext-real Element of REAL
AB is V11() real ext-real Element of REAL
AB (#) H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(AB (#) H) `| b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((AB (#) H) `| b) . T is V11() real ext-real Element of REAL
diff (H,T) is V11() real ext-real Element of REAL
AB * (diff (H,T)) is V11() real ext-real Element of REAL
(H `| b) . T is V11() real ext-real Element of REAL
rseq . T is V11() real ext-real Element of REAL
(a (#) rseq) . T is V11() real ext-real Element of REAL
(a (#) rseq) | b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((a (#) rseq) | b) . T is V11() real ext-real Element of REAL
dom ((a (#) rseq) | b) is V50() V51() V52() Element of K6(REAL)
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b (#) rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H (#) rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b (#) AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H (#) rseq) + (b (#) AB) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom b is V50() V51() V52() Element of K6(REAL)
rseq `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (AB | a) is V50() V51() V52() Element of K6(REAL)
dom AB is V50() V51() V52() Element of K6(REAL)
(dom AB) /\ a is V50() V51() V52() Element of K6(REAL)
(dom b) /\ (dom AB) is V50() V51() V52() Element of K6(REAL)
dom (b (#) AB) is V50() V51() V52() Element of K6(REAL)
dom rseq is V50() V51() V52() Element of K6(REAL)
b `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (H | a) is V50() V51() V52() Element of K6(REAL)
dom H is V50() V51() V52() Element of K6(REAL)
(dom H) /\ a is V50() V51() V52() Element of K6(REAL)
(dom H) /\ (dom rseq) is V50() V51() V52() Element of K6(REAL)
dom (H (#) rseq) is V50() V51() V52() Element of K6(REAL)
(dom (H (#) rseq)) /\ (dom (b (#) AB)) is V50() V51() V52() Element of K6(REAL)
dom ((H (#) rseq) + (b (#) AB)) is V50() V51() V52() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(b (#) rseq) `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((b (#) rseq) `| a) is V50() V51() V52() Element of K6(REAL)
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq `| a) . T is V11() real ext-real Element of REAL
diff (rseq,T) is V11() real ext-real Element of REAL
AB . T is V11() real ext-real Element of REAL
(b (#) AB) . T is V11() real ext-real Element of REAL
b . T is V11() real ext-real Element of REAL
(b . T) * (diff (rseq,T)) is V11() real ext-real Element of REAL
(b `| a) . T is V11() real ext-real Element of REAL
diff (b,T) is V11() real ext-real Element of REAL
H . T is V11() real ext-real Element of REAL
(H (#) rseq) . T is V11() real ext-real Element of REAL
rseq . T is V11() real ext-real Element of REAL
(rseq . T) * (diff (b,T)) is V11() real ext-real Element of REAL
rseq | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((b (#) rseq) `| a) . T is V11() real ext-real Element of REAL
diff ((b (#) rseq),T) is V11() real ext-real Element of REAL
((rseq . T) * (diff (b,T))) + ((b . T) * (diff (rseq,T))) is V11() real ext-real Element of REAL
(b (#) AB) + (H (#) rseq) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((b (#) AB) + (H (#) rseq)) . T is V11() real ext-real Element of REAL
((b (#) AB) + (H (#) rseq)) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(((b (#) AB) + (H (#) rseq)) | a) . T is V11() real ext-real Element of REAL
((H (#) rseq) + (b (#) AB)) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (((H (#) rseq) + (b (#) AB)) | a) is V50() V51() V52() Element of K6(REAL)
a is set
b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b (#) b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H / b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq (#) b is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H (#) AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq (#) b) - (H (#) AB) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
- (H (#) AB) is V13() V16( REAL ) V18() V40() V41() V42() set
- 1 is V11() real ext-real V89() set
(- 1) (#) (H (#) AB) is V13() V16( REAL ) V18() V40() V41() V42() set
(rseq (#) b) + (- (H (#) AB)) is V13() V16( REAL ) V18() V40() V41() V42() set
((rseq (#) b) - (H (#) AB)) / (b (#) b) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom H is V50() V51() V52() Element of K6(REAL)
b `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (AB | a) is V50() V51() V52() Element of K6(REAL)
dom AB is V50() V51() V52() Element of K6(REAL)
(dom AB) /\ a is V50() V51() V52() Element of K6(REAL)
(dom H) /\ (dom AB) is V50() V51() V52() Element of K6(REAL)
dom (H (#) AB) is V50() V51() V52() Element of K6(REAL)
dom b is V50() V51() V52() Element of K6(REAL)
H `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (rseq | a) is V50() V51() V52() Element of K6(REAL)
dom rseq is V50() V51() V52() Element of K6(REAL)
(dom rseq) /\ a is V50() V51() V52() Element of K6(REAL)
(dom rseq) /\ (dom b) is V50() V51() V52() Element of K6(REAL)
dom (rseq (#) b) is V50() V51() V52() Element of K6(REAL)
(dom (rseq (#) b)) /\ (dom (H (#) AB)) is V50() V51() V52() Element of K6(REAL)
dom ((rseq (#) b) - (H (#) AB)) is V50() V51() V52() Element of K6(REAL)
(dom b) /\ a is V50() V51() V52() Element of K6(REAL)
b | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (b | a) is V50() V51() V52() Element of K6(REAL)
T is V11() real ext-real Element of REAL
(H / b) `| a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((H / b) `| a) is V50() V51() V52() Element of K6(REAL)
H | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
b . T is V11() real ext-real Element of REAL
(b | a) . T is V11() real ext-real Element of REAL
(b . T) ^2 is V11() real ext-real Element of REAL
(b . T) * (b . T) is V11() real ext-real set
(b | a) (#) (b | a) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((b | a) (#) (b | a)) . T is V11() real ext-real Element of REAL
L1 is set
b . L1 is V11() real ext-real Element of REAL
(b | a) . L1 is V11() real ext-real Element of REAL
{0} is non empty V50() V51() V52() V53() V54() V55() left_end bounded_below Element of K6(REAL)
(b | a) " {0} is V50() V51() V52() Element of K6(REAL)
(dom (b | a)) \ ((b | a) " {0}) is V50() V51() V52() Element of K6(REAL)
((dom (b | a)) \ ((b | a) " {0})) /\ ((dom (b | a)) \ ((b | a) " {0})) is V50() V51() V52() Element of K6(REAL)
dom ((b | a) (#) (b | a)) is V50() V51() V52() Element of K6(REAL)
((b | a) (#) (b | a)) " {0} is V50() V51() V52() Element of K6(REAL)
(dom ((b | a) (#) (b | a))) \ (((b | a) (#) (b | a)) " {0}) is V50() V51() V52() Element of K6(REAL)
(dom ((rseq (#) b) - (H (#) AB))) /\ ((dom ((b | a) (#) (b | a))) \ (((b | a) (#) (b | a)) " {0})) is V50() V51() V52() Element of K6(REAL)
((rseq (#) b) - (H (#) AB)) / ((b | a) (#) (b | a)) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (((rseq (#) b) - (H (#) AB)) / ((b | a) (#) (b | a))) is V50() V51() V52() Element of K6(REAL)
(b `| a) . T is V11() real ext-real Element of REAL
diff (b,T) is V11() real ext-real Element of REAL
AB . T is V11() real ext-real Element of REAL
(H (#) AB) . T is V11() real ext-real Element of REAL
H . T is V11() real ext-real Element of REAL
(H . T) * (diff (b,T)) is V11() real ext-real Element of REAL
(H `| a) . T is V11() real ext-real Element of REAL
diff (H,T) is V11() real ext-real Element of REAL
rseq . T is V11() real ext-real Element of REAL
(rseq (#) b) . T is V11() real ext-real Element of REAL
(b . T) * (diff (H,T)) is V11() real ext-real Element of REAL
((rseq (#) b) - (H (#) AB)) . T is V11() real ext-real Element of REAL
(diff (H,T)) * (b . T) is V11() real ext-real Element of REAL
(diff (b,T)) * (H . T) is V11() real ext-real Element of REAL
((diff (H,T)) * (b . T)) - ((diff (b,T)) * (H . T)) is V11() real ext-real Element of REAL
- ((diff (b,T)) * (H . T)) is V11() real ext-real set
((diff (H,T)) * (b . T)) + (- ((diff (b,T)) * (H . T))) is V11() real ext-real set
((H / b) `| a) . T is V11() real ext-real Element of REAL
diff ((H / b),T) is V11() real ext-real Element of REAL
(((diff (H,T)) * (b . T)) - ((diff (b,T)) * (H . T))) / ((b . T) ^2) is V11() real ext-real Element of REAL
((b . T) ^2) " is V11() real ext-real set
(((diff (H,T)) * (b . T)) - ((diff (b,T)) * (H . T))) * (((b . T) ^2) ") is V11() real ext-real set
(((rseq (#) b) - (H (#) AB)) / ((b | a) (#) (b | a))) . T is V11() real ext-real Element of REAL
(b (#) b) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq (#) b) - (H (#) AB)) / ((b (#) b) | a) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(((rseq (#) b) - (H (#) AB)) / ((b (#) b) | a)) . T is V11() real ext-real Element of REAL
(((rseq (#) b) - (H (#) AB)) / (b (#) b)) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((((rseq (#) b) - (H (#) AB)) / (b (#) b)) | a) . T is V11() real ext-real Element of REAL
T is set
(b | a) . T is V11() real ext-real Element of REAL
b . T is V11() real ext-real Element of REAL
((rseq (#) b) - (H (#) AB)) | a is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (((rseq (#) b) - (H (#) AB)) | a) is V50() V51() V52() Element of K6(REAL)
(dom (((rseq (#) b) - (H (#) AB)) | a)) /\ ((dom ((b | a) (#) (b | a))) \ (((b | a) (#) (b | a)) " {0})) is V50() V51() V52() Element of K6(REAL)
(((rseq (#) b) - (H (#) AB)) | a) / ((b | a) (#) (b | a)) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((((rseq (#) b) - (H (#) AB)) | a) / ((b | a) (#) (b | a))) is V50() V51() V52() Element of K6(REAL)
(((rseq (#) b) - (H (#) AB)) | a) / ((b (#) b) | a) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((((rseq (#) b) - (H (#) AB)) | a) / ((b (#) b) | a)) is V50() V51() V52() Element of K6(REAL)
dom ((((rseq (#) b) - (H (#) AB)) / (b (#) b)) | a) is V50() V51() V52() Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
].a,b.[ is V50() V51() V52() open non left_end non right_end V100() Element of K6(REAL)
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom H is V50() V51() V52() Element of K6(REAL)
H | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom rseq is V50() V51() V52() Element of K6(REAL)
rseq . a is V11() real ext-real Element of REAL
rseq | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (rseq | ].a,b.[) is V50() V51() V52() Element of K6(REAL)
(dom rseq) /\ ].a,b.[ is V50() V51() V52() Element of K6(REAL)
REAL --> (rseq . a) is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
(REAL --> (rseq . a)) | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
K1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom K1 is V50() V51() V52() Element of K6(REAL)
dom (REAL --> (rseq . a)) is V50() V51() V52() Element of K6(REAL)
(dom (REAL --> (rseq . a))) /\ ].a,b.[ is V50() V51() V52() Element of K6(REAL)
REAL /\ ].a,b.[ is V50() V51() V52() V100() Element of K6(REAL)
r is V11() real ext-real Element of REAL
].a,b.[ /\ (dom K1) is V50() V51() V52() Element of K6(REAL)
K1 . r is V11() real ext-real Element of REAL
H0 is V11() real ext-real set
(REAL --> (rseq . a)) . H0 is V11() real ext-real Element of REAL
K1 /. r is V11() real ext-real Element of REAL
K1 | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
K is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom K is V50() V51() V52() Element of K6(REAL)
dom L1 is V50() V51() V52() Element of K6(REAL)
(dom L1) /\ ].a,b.[ is V50() V51() V52() Element of K6(REAL)
r is V11() real ext-real set
K . r is V11() real ext-real Element of REAL
L1 . r is V11() real ext-real Element of REAL
H0 is V11() real ext-real Element of REAL
integral (H,a,H0) is V11() real ext-real Element of REAL
integral (H,a,r) is V11() real ext-real Element of REAL
r is set
H0 is V11() real ext-real set
K1 . r is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
(REAL --> (rseq . a)) . p is V11() real ext-real Element of REAL
(rseq | ].a,b.[) . r is V11() real ext-real Element of REAL
rseq . H0 is V11() real ext-real Element of REAL
integral (H,a,H0) is V11() real ext-real Element of REAL
(integral (H,a,H0)) + (rseq . a) is V11() real ext-real Element of REAL
K . r is V11() real ext-real Element of REAL
(K . r) + (K1 . r) is V11() real ext-real Element of REAL
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
r is V11() real ext-real Element of REAL
diff (K,r) is V11() real ext-real Element of REAL
H . r is V11() real ext-real Element of REAL
H | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (H | ].a,b.[) is V50() V51() V52() Element of K6(REAL)
H0 is V11() real ext-real set
H . H0 is V11() real ext-real Element of REAL
p is V11() real ext-real set
e is V11() real ext-real set
H0 - e is V11() real ext-real set
- e is V11() real ext-real set
H0 + (- e) is V11() real ext-real set
H0 + e is V11() real ext-real set
].(H0 - e),(H0 + e).[ is V50() V51() V52() open non left_end non right_end V100() Element of K6(REAL)
(H | ].a,b.[) . H0 is V11() real ext-real Element of REAL
N is V11() real ext-real set
min (e,N) is V11() real ext-real set
n is V11() real ext-real set
n - H0 is V11() real ext-real set
- H0 is V11() real ext-real set
n + (- H0) is V11() real ext-real set
abs (n - H0) is V11() real ext-real Element of REAL
].a,b.[ /\ (dom H) is V50() V51() V52() Element of K6(REAL)
H . n is V11() real ext-real Element of REAL
(H . n) - (H . H0) is V11() real ext-real Element of REAL
- (H . H0) is V11() real ext-real set
(H . n) + (- (H . H0)) is V11() real ext-real set
abs ((H . n) - (H . H0)) is V11() real ext-real Element of REAL
(H | ].a,b.[) . n is V11() real ext-real Element of REAL
((H | ].a,b.[) . n) - (H . H0) is V11() real ext-real Element of REAL
((H | ].a,b.[) . n) + (- (H . H0)) is V11() real ext-real set
abs (((H | ].a,b.[) . n) - (H . H0)) is V11() real ext-real Element of REAL
((H | ].a,b.[) . n) - ((H | ].a,b.[) . H0) is V11() real ext-real Element of REAL
- ((H | ].a,b.[) . H0) is V11() real ext-real set
((H | ].a,b.[) . n) + (- ((H | ].a,b.[) . H0)) is V11() real ext-real set
abs (((H | ].a,b.[) . n) - ((H | ].a,b.[) . H0)) is V11() real ext-real Element of REAL
n is V11() real ext-real set
n - H0 is V11() real ext-real set
n + (- H0) is V11() real ext-real set
abs (n - H0) is V11() real ext-real Element of REAL
H . n is V11() real ext-real Element of REAL
(H . n) - (H . H0) is V11() real ext-real Element of REAL
(H . n) + (- (H . H0)) is V11() real ext-real set
abs ((H . n) - (H . H0)) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(dom K) /\ (dom K1) is V50() V51() V52() Element of K6(REAL)
K + K1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
r is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
rseq `| ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (rseq `| ].a,b.[) is V50() V51() V52() Element of K6(REAL)
(dom H) /\ ].a,b.[ is V50() V51() V52() Element of K6(REAL)
H | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (H | ].a,b.[) is V50() V51() V52() Element of K6(REAL)
(rseq `| ].a,b.[) . r is V11() real ext-real Element of REAL
(rseq | ].a,b.[) `| ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq | ].a,b.[) `| ].a,b.[) . r is V11() real ext-real Element of REAL
diff (K,r) is V11() real ext-real Element of REAL
diff (K1,r) is V11() real ext-real Element of REAL
(diff (K,r)) + (diff (K1,r)) is V11() real ext-real Element of REAL
H . r is V11() real ext-real Element of REAL
(H . r) + (diff (K1,r)) is V11() real ext-real Element of REAL
K1 `| ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(K1 `| ].a,b.[) . r is V11() real ext-real Element of REAL
(H | ].a,b.[) . r is V11() real ext-real Element of REAL
].a,b.[ /\ (dom H) is V50() V51() V52() Element of K6(REAL)
a is V11() real ext-real set
b is V11() real ext-real set
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
].a,b.[ is V50() V51() V52() open non left_end non right_end V100() Element of K6(REAL)
H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H | [.a,b.] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom H is V50() V51() V52() Element of K6(REAL)
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB is V11() real ext-real set
T is V11() real ext-real set
rseq . AB is V11() real ext-real Element of REAL
integral (H,T,AB) is V11() real ext-real Element of REAL
rseq . T is V11() real ext-real Element of REAL
(integral (H,T,AB)) + (rseq . T) is V11() real ext-real Element of REAL
rseq `| ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H | ].a,b.[ is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
[.AB,T.] is V50() V51() V52() closed V100() Element of K6(REAL)
['AB,T'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H | ['AB,T'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq `| ].a,b.[) || ['AB,T'] is V13() V16(['AB,T']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['AB,T'],REAL))
K7(['AB,T'],REAL) is V40() V41() V42() set
K6(K7(['AB,T'],REAL)) is set
(H | ].a,b.[) | ['AB,T'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H || ['AB,T'] is V13() V16(['AB,T']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['AB,T'],REAL))
(rseq `| ].a,b.[) | ['AB,T'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((H | ].a,b.[),AB,T) is V11() real ext-real Element of REAL
(integral ((H | ].a,b.[),AB,T)) + (rseq . AB) is V11() real ext-real Element of REAL
integral ((H | ].a,b.[),['AB,T']) is V11() real ext-real Element of REAL
(H | ].a,b.[) || ['AB,T'] is V13() V16(['AB,T']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['AB,T'],REAL))
integral ((H | ].a,b.[) || ['AB,T']) is V11() real ext-real Element of REAL
upper_integral ((H | ].a,b.[) || ['AB,T']) is V11() real ext-real Element of REAL
upper_sum_set ((H | ].a,b.[) || ['AB,T']) is non empty V13() V16( divs ['AB,T']) V17( REAL ) V18() total V27( divs ['AB,T'], REAL ) V40() V41() V42() Element of K6(K7((divs ['AB,T']),REAL))
divs ['AB,T'] is non empty set
K7((divs ['AB,T']),REAL) is V40() V41() V42() set
K6(K7((divs ['AB,T']),REAL)) is set
rng (upper_sum_set ((H | ].a,b.[) || ['AB,T'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((H | ].a,b.[) || ['AB,T']))) is V11() real ext-real Element of REAL
(integral ((H | ].a,b.[),['AB,T'])) + (rseq . AB) is V11() real ext-real Element of REAL
integral (H,['AB,T']) is V11() real ext-real Element of REAL
integral (H || ['AB,T']) is V11() real ext-real Element of REAL
upper_integral (H || ['AB,T']) is V11() real ext-real Element of REAL
upper_sum_set (H || ['AB,T']) is non empty V13() V16( divs ['AB,T']) V17( REAL ) V18() total V27( divs ['AB,T'], REAL ) V40() V41() V42() Element of K6(K7((divs ['AB,T']),REAL))
rng (upper_sum_set (H || ['AB,T'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (H || ['AB,T']))) is V11() real ext-real Element of REAL
(integral (H,['AB,T'])) + (rseq . AB) is V11() real ext-real Element of REAL
integral (H,AB,T) is V11() real ext-real Element of REAL
(integral (H,AB,T)) + (rseq . AB) is V11() real ext-real Element of REAL
- (integral (H,['AB,T'])) is V11() real ext-real Element of REAL
- (integral (H,AB,T)) is V11() real ext-real Element of REAL
[.T,AB.] is V50() V51() V52() closed V100() Element of K6(REAL)
['T,AB'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H | ['T,AB'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq `| ].a,b.[) || ['T,AB'] is V13() V16(['T,AB']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['T,AB'],REAL))
K7(['T,AB'],REAL) is V40() V41() V42() set
K6(K7(['T,AB'],REAL)) is set
(H | ].a,b.[) | ['T,AB'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H || ['T,AB'] is V13() V16(['T,AB']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['T,AB'],REAL))
integral ((H | ].a,b.[),T,AB) is V11() real ext-real Element of REAL
(integral ((H | ].a,b.[),T,AB)) + (rseq . T) is V11() real ext-real Element of REAL
integral ((H | ].a,b.[),['T,AB']) is V11() real ext-real Element of REAL
(H | ].a,b.[) || ['T,AB'] is V13() V16(['T,AB']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['T,AB'],REAL))
integral ((H | ].a,b.[) || ['T,AB']) is V11() real ext-real Element of REAL
upper_integral ((H | ].a,b.[) || ['T,AB']) is V11() real ext-real Element of REAL
upper_sum_set ((H | ].a,b.[) || ['T,AB']) is non empty V13() V16( divs ['T,AB']) V17( REAL ) V18() total V27( divs ['T,AB'], REAL ) V40() V41() V42() Element of K6(K7((divs ['T,AB']),REAL))
divs ['T,AB'] is non empty set
K7((divs ['T,AB']),REAL) is V40() V41() V42() set
K6(K7((divs ['T,AB']),REAL)) is set
rng (upper_sum_set ((H | ].a,b.[) || ['T,AB'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((H | ].a,b.[) || ['T,AB']))) is V11() real ext-real Element of REAL
(integral ((H | ].a,b.[),['T,AB'])) + (rseq . T) is V11() real ext-real Element of REAL
integral (H,['T,AB']) is V11() real ext-real Element of REAL
integral (H || ['T,AB']) is V11() real ext-real Element of REAL
upper_integral (H || ['T,AB']) is V11() real ext-real Element of REAL
upper_sum_set (H || ['T,AB']) is non empty V13() V16( divs ['T,AB']) V17( REAL ) V18() total V27( divs ['T,AB'], REAL ) V40() V41() V42() Element of K6(K7((divs ['T,AB']),REAL))
rng (upper_sum_set (H || ['T,AB'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (H || ['T,AB']))) is V11() real ext-real Element of REAL
(integral (H,['T,AB'])) + (rseq . T) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq . b is V11() real ext-real Element of REAL
rseq . a is V11() real ext-real Element of REAL
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral (AB,a,b) is V11() real ext-real Element of REAL
(integral (AB,a,b)) + (rseq . a) is V11() real ext-real Element of REAL
rseq `| H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V40() V41() V42() set
K6(K7(['a,b'],REAL)) is set
(rseq `| H) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
(AB | H) | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((AB | H),a,b) is V11() real ext-real Element of REAL
(integral ((AB | H),a,b)) + (rseq . a) is V11() real ext-real Element of REAL
integral ((AB | H),['a,b']) is V11() real ext-real Element of REAL
(AB | H) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
integral ((AB | H) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral ((AB | H) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((AB | H) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (upper_sum_set ((AB | H) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((AB | H) || ['a,b']))) is V11() real ext-real Element of REAL
(integral ((AB | H),['a,b'])) + (rseq . a) is V11() real ext-real Element of REAL
integral (AB,['a,b']) is V11() real ext-real Element of REAL
integral (AB || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (AB || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (AB || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set (AB || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (AB || ['a,b']))) is V11() real ext-real Element of REAL
(integral (AB,['a,b'])) + (rseq . a) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom rseq is V50() V51() V52() Element of K6(REAL)
rseq | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
H is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom rseq is V50() V51() V52() Element of K6(REAL)
rseq | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral (rseq,a,b) is V11() real ext-real Element of REAL
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB . b is V11() real ext-real Element of REAL
AB . a is V11() real ext-real Element of REAL
(integral (rseq,a,b)) + (AB . a) is V11() real ext-real Element of REAL
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
rseq | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom rseq is V50() V51() V52() Element of K6(REAL)
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom AB is V50() V51() V52() Element of K6(REAL)
T is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T . b is V11() real ext-real Element of REAL
T . a is V11() real ext-real Element of REAL
T (#) AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((T (#) AB),a,b) is V11() real ext-real Element of REAL
L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 . b is V11() real ext-real Element of REAL
(T . b) * (L1 . b) is V11() real ext-real Element of REAL
L1 . a is V11() real ext-real Element of REAL
(T . a) * (L1 . a) is V11() real ext-real Element of REAL
((T . b) * (L1 . b)) - ((T . a) * (L1 . a)) is V11() real ext-real Element of REAL
- ((T . a) * (L1 . a)) is V11() real ext-real set
((T . b) * (L1 . b)) + (- ((T . a) * (L1 . a))) is V11() real ext-real set
rseq (#) L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((rseq (#) L1),a,b) is V11() real ext-real Element of REAL
(integral ((rseq (#) L1),a,b)) + (integral ((T (#) AB),a,b)) is V11() real ext-real Element of REAL
dom L1 is V50() V51() V52() Element of K6(REAL)
L1 | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
['a,b'] /\ ['a,b'] is V50() V51() V52() V100() Element of K6(REAL)
(rseq (#) L1) | (['a,b'] /\ ['a,b']) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom T is V50() V51() V52() Element of K6(REAL)
T | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(T (#) AB) | (['a,b'] /\ ['a,b']) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq (#) L1) + (T (#) AB) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq (#) L1) + (T (#) AB)) | (['a,b'] /\ ['a,b']) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T `| H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 `| H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T (#) L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(T (#) L1) `| H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq | H) (#) L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T (#) (AB | H) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq | H) (#) L1) + (T (#) (AB | H)) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(rseq (#) L1) | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq (#) L1) | H) + (T (#) (AB | H)) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(T (#) AB) | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq (#) L1) | H) + ((T (#) AB) | H) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((rseq (#) L1) + (T (#) AB)) | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
min (a,b) is V11() real ext-real set
max (a,b) is V11() real ext-real set
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
(dom T) /\ (dom AB) is V50() V51() V52() Element of K6(REAL)
dom (T (#) AB) is V50() V51() V52() Element of K6(REAL)
(dom rseq) /\ (dom L1) is V50() V51() V52() Element of K6(REAL)
dom (rseq (#) L1) is V50() V51() V52() Element of K6(REAL)
(T (#) L1) . b is V11() real ext-real Element of REAL
integral (((rseq (#) L1) + (T (#) AB)),a,b) is V11() real ext-real Element of REAL
(T (#) L1) . a is V11() real ext-real Element of REAL
(integral (((rseq (#) L1) + (T (#) AB)),a,b)) + ((T (#) L1) . a) is V11() real ext-real Element of REAL
((T (#) L1) . b) - ((T (#) L1) . a) is V11() real ext-real Element of REAL
- ((T (#) L1) . a) is V11() real ext-real set
((T (#) L1) . b) + (- ((T (#) L1) . a)) is V11() real ext-real set
a is V11() real ext-real set
b is V11() real ext-real set
[.a,b.] is V50() V51() V52() closed V100() Element of K6(REAL)
H is set
rseq is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom rseq is V50() V51() V52() Element of K6(REAL)
rseq | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom AB is V50() V51() V52() Element of K6(REAL)
AB | H is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
T . b is V11() real ext-real Element of REAL
T . a is V11() real ext-real Element of REAL
T (#) AB is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((T (#) AB),a,b) is V11() real ext-real Element of REAL
L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
L1 . b is V11() real ext-real Element of REAL
(T . b) * (L1 . b) is V11() real ext-real Element of REAL
L1 . a is V11() real ext-real Element of REAL
(T . a) * (L1 . a) is V11() real ext-real Element of REAL
((T . b) * (L1 . b)) - ((T . a) * (L1 . a)) is V11() real ext-real Element of REAL
- ((T . a) * (L1 . a)) is V11() real ext-real set
((T . b) * (L1 . b)) + (- ((T . a) * (L1 . a))) is V11() real ext-real set
rseq (#) L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((rseq (#) L1),a,b) is V11() real ext-real Element of REAL
(integral ((rseq (#) L1),a,b)) + (integral ((T (#) AB),a,b)) is V11() real ext-real Element of REAL
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
rseq | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
AB | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
cos | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (cos | REAL) is V50() V51() V52() Element of K6(REAL)
REAL /\ REAL is V50() V51() V52() V100() set
a is set
sin `| REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (sin `| REAL) is V50() V51() V52() Element of K6(REAL)
(sin `| REAL) . a is V11() real ext-real Element of REAL
b is V11() real ext-real set
diff (sin,b) is V11() real ext-real Element of REAL
cos . b is V11() real ext-real Element of REAL
(cos | REAL) . a is V11() real ext-real Element of REAL
a is V11() real ext-real set
sin . a is V11() real ext-real Element of REAL
b is V11() real ext-real set
sin . b is V11() real ext-real Element of REAL
(sin . a) - (sin . b) is V11() real ext-real Element of REAL
- (sin . b) is V11() real ext-real set
(sin . a) + (- (sin . b)) is V11() real ext-real set
integral (cos,b,a) is V11() real ext-real Element of REAL
min (b,a) is V11() real ext-real set
max (b,a) is V11() real ext-real set
[.(min (b,a)),(max (b,a)).] is V50() V51() V52() closed V100() Element of K6(REAL)
cos | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
sin . (max (b,a)) is V11() real ext-real Element of REAL
integral (cos,(min (b,a)),(max (b,a))) is V11() real ext-real Element of REAL
sin . (min (b,a)) is V11() real ext-real Element of REAL
(integral (cos,(min (b,a)),(max (b,a)))) + (sin . (min (b,a))) is V11() real ext-real Element of REAL
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
integral (cos,['a,b']) is V11() real ext-real Element of REAL
cos || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V40() V41() V42() set
K6(K7(['a,b'],REAL)) is set
integral (cos || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (cos || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (cos || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (upper_sum_set (cos || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (cos || ['a,b']))) is V11() real ext-real Element of REAL
- (integral (cos,['a,b'])) is V11() real ext-real Element of REAL
- (integral (cos,b,a)) is V11() real ext-real Element of REAL
(- (integral (cos,b,a))) + (sin . a) is V11() real ext-real Element of REAL
- 1 is V11() real ext-real V89() Element of REAL
(- 1) (#) cos is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
sin | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (sin | REAL) is V50() V51() V52() Element of K6(REAL)
REAL /\ REAL is V50() V51() V52() V100() set
dom ((- 1) (#) cos) is V50() V51() V52() Element of K6(REAL)
a is set
((- 1) (#) cos) `| REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (((- 1) (#) cos) `| REAL) is V50() V51() V52() Element of K6(REAL)
(((- 1) (#) cos) `| REAL) . a is V11() real ext-real Element of REAL
b is V11() real ext-real set
diff (cos,b) is V11() real ext-real Element of REAL
(- 1) * (diff (cos,b)) is V11() real ext-real Element of REAL
sin . b is V11() real ext-real Element of REAL
- (sin . b) is V11() real ext-real Element of REAL
(- 1) * (- (sin . b)) is V11() real ext-real Element of REAL
(sin | REAL) . a is V11() real ext-real Element of REAL
a is V11() real ext-real set
cos . a is V11() real ext-real Element of REAL
b is V11() real ext-real set
cos . b is V11() real ext-real Element of REAL
(cos . a) - (cos . b) is V11() real ext-real Element of REAL
- (cos . b) is V11() real ext-real set
(cos . a) + (- (cos . b)) is V11() real ext-real set
integral (sin,a,b) is V11() real ext-real Element of REAL
min (a,b) is V11() real ext-real set
max (a,b) is V11() real ext-real set
dom ((- 1) (#) cos) is V50() V51() V52() Element of K6(REAL)
[.(min (a,b)),(max (a,b)).] is V50() V51() V52() closed V100() Element of K6(REAL)
sin | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
((- 1) (#) cos) . (max (a,b)) is V11() real ext-real Element of REAL
integral (sin,(min (a,b)),(max (a,b))) is V11() real ext-real Element of REAL
((- 1) (#) cos) . (min (a,b)) is V11() real ext-real Element of REAL
(integral (sin,(min (a,b)),(max (a,b)))) + (((- 1) (#) cos) . (min (a,b))) is V11() real ext-real Element of REAL
cos . (max (a,b)) is V11() real ext-real Element of REAL
(- 1) * (cos . (max (a,b))) is V11() real ext-real Element of REAL
cos . (min (a,b)) is V11() real ext-real Element of REAL
(- 1) * (cos . (min (a,b))) is V11() real ext-real Element of REAL
(integral (sin,(min (a,b)),(max (a,b)))) + ((- 1) * (cos . (min (a,b)))) is V11() real ext-real Element of REAL
(cos . (min (a,b))) - (cos . (max (a,b))) is V11() real ext-real Element of REAL
- (cos . (max (a,b))) is V11() real ext-real set
(cos . (min (a,b))) + (- (cos . (max (a,b)))) is V11() real ext-real set
['b,a'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
integral (sin,['b,a']) is V11() real ext-real Element of REAL
sin || ['b,a'] is V13() V16(['b,a']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['b,a'],REAL))
K7(['b,a'],REAL) is V40() V41() V42() set
K6(K7(['b,a'],REAL)) is set
integral (sin || ['b,a']) is V11() real ext-real Element of REAL
upper_integral (sin || ['b,a']) is V11() real ext-real Element of REAL
upper_sum_set (sin || ['b,a']) is non empty V13() V16( divs ['b,a']) V17( REAL ) V18() total V27( divs ['b,a'], REAL ) V40() V41() V42() Element of K6(K7((divs ['b,a']),REAL))
divs ['b,a'] is non empty set
K7((divs ['b,a']),REAL) is V40() V41() V42() set
K6(K7((divs ['b,a']),REAL)) is set
rng (upper_sum_set (sin || ['b,a'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (sin || ['b,a']))) is V11() real ext-real Element of REAL
- (integral (sin,['b,a'])) is V11() real ext-real Element of REAL
integral (sin,b,a) is V11() real ext-real Element of REAL
- (integral (sin,b,a)) is V11() real ext-real Element of REAL
exp_R | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (exp_R | REAL) is V50() V51() V52() Element of K6(REAL)
REAL /\ REAL is V50() V51() V52() V100() set
a is set
exp_R `| REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (exp_R `| REAL) is V50() V51() V52() Element of K6(REAL)
b is V11() real ext-real set
(exp_R `| REAL) . a is V11() real ext-real Element of REAL
diff (exp_R,b) is V11() real ext-real Element of REAL
H is V11() real ext-real Element of REAL
exp_R . H is V11() real ext-real Element of REAL
(exp_R | REAL) . a is V11() real ext-real Element of REAL
a is V11() real ext-real set
exp_R . a is V11() real ext-real Element of REAL
b is V11() real ext-real set
exp_R . b is V11() real ext-real Element of REAL
(exp_R . a) - (exp_R . b) is V11() real ext-real Element of REAL
- (exp_R . b) is V11() real ext-real set
(exp_R . a) + (- (exp_R . b)) is V11() real ext-real set
integral (exp_R,b,a) is V11() real ext-real Element of REAL
min (b,a) is V11() real ext-real set
max (b,a) is V11() real ext-real set
[.(min (b,a)),(max (b,a)).] is V50() V51() V52() closed V100() Element of K6(REAL)
exp_R | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
exp_R . (max (b,a)) is V11() real ext-real Element of REAL
integral (exp_R,(min (b,a)),(max (b,a))) is V11() real ext-real Element of REAL
exp_R . (min (b,a)) is V11() real ext-real Element of REAL
(integral (exp_R,(min (b,a)),(max (b,a)))) + (exp_R . (min (b,a))) is V11() real ext-real Element of REAL
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
integral (exp_R,['a,b']) is V11() real ext-real Element of REAL
exp_R || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V40() V41() V42() set
K6(K7(['a,b'],REAL)) is set
integral (exp_R || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (exp_R || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (exp_R || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (upper_sum_set (exp_R || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (exp_R || ['a,b']))) is V11() real ext-real Element of REAL
- (integral (exp_R,['a,b'])) is V11() real ext-real Element of REAL
- (integral (exp_R,b,a)) is V11() real ext-real Element of REAL
(- (integral (exp_R,b,a))) + (exp_R . a) is V11() real ext-real Element of REAL
a is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
a + 1 is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
#Z (a + 1) is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
#Z a is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
(a + 1) (#) (#Z a) is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
((a + 1) (#) (#Z a)) | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (((a + 1) (#) (#Z a)) | REAL) is V50() V51() V52() Element of K6(REAL)
dom ((a + 1) (#) (#Z a)) is V50() V51() V52() Element of K6(REAL)
(dom ((a + 1) (#) (#Z a))) /\ REAL is V50() V51() V52() Element of K6(REAL)
REAL /\ REAL is V50() V51() V52() V100() set
dom (#Z (a + 1)) is V50() V51() V52() Element of K6(REAL)
(#Z (a + 1)) | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
H is V11() real ext-real Element of REAL
dom (#Z a) is V50() V51() V52() Element of K6(REAL)
H is set
(#Z (a + 1)) `| REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom ((#Z (a + 1)) `| REAL) is V50() V51() V52() Element of K6(REAL)
((#Z (a + 1)) `| REAL) . H is V11() real ext-real Element of REAL
rseq is V11() real ext-real set
diff ((#Z (a + 1)),rseq) is V11() real ext-real Element of REAL
b is natural V11() real ext-real V89() set
b - 1 is V11() real ext-real V89() Element of REAL
- 1 is V11() real ext-real V89() set
b + (- 1) is V11() real ext-real V89() set
rseq #Z (b - 1) is V11() real ext-real set
b * (rseq #Z (b - 1)) is V11() real ext-real set
(#Z a) . H is V11() real ext-real Element of REAL
(a + 1) * ((#Z a) . H) is V11() real ext-real Element of REAL
((a + 1) (#) (#Z a)) . H is V11() real ext-real Element of REAL
(((a + 1) (#) (#Z a)) | REAL) . H is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
H is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H + 1 is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
#Z (H + 1) is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
(#Z (H + 1)) . a is V11() real ext-real Element of REAL
(#Z (H + 1)) . b is V11() real ext-real Element of REAL
((#Z (H + 1)) . a) - ((#Z (H + 1)) . b) is V11() real ext-real Element of REAL
- ((#Z (H + 1)) . b) is V11() real ext-real set
((#Z (H + 1)) . a) + (- ((#Z (H + 1)) . b)) is V11() real ext-real set
#Z H is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
(H + 1) (#) (#Z H) is non empty V13() V16( REAL ) V17( REAL ) V18() total V27( REAL , REAL ) V40() V41() V42() Element of K6(K7(REAL,REAL))
integral (((H + 1) (#) (#Z H)),b,a) is V11() real ext-real Element of REAL
dom ((H + 1) (#) (#Z H)) is V50() V51() V52() Element of K6(REAL)
dom (#Z H) is V50() V51() V52() Element of K6(REAL)
(#Z H) | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
rseq is V11() real ext-real Element of REAL
((H + 1) (#) (#Z H)) | REAL is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
min (b,a) is V11() real ext-real set
max (b,a) is V11() real ext-real set
[.(min (b,a)),(max (b,a)).] is V50() V51() V52() closed V100() Element of K6(REAL)
(#Z (H + 1)) . (max (b,a)) is V11() real ext-real Element of REAL
integral (((H + 1) (#) (#Z H)),(min (b,a)),(max (b,a))) is V11() real ext-real Element of REAL
(#Z (H + 1)) . (min (b,a)) is V11() real ext-real Element of REAL
(integral (((H + 1) (#) (#Z H)),(min (b,a)),(max (b,a)))) + ((#Z (H + 1)) . (min (b,a))) is V11() real ext-real Element of REAL
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
integral (((H + 1) (#) (#Z H)),['a,b']) is V11() real ext-real Element of REAL
((H + 1) (#) (#Z H)) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
K7(['a,b'],REAL) is V40() V41() V42() set
K6(K7(['a,b'],REAL)) is set
integral (((H + 1) (#) (#Z H)) || ['a,b']) is V11() real ext-real Element of REAL
upper_integral (((H + 1) (#) (#Z H)) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set (((H + 1) (#) (#Z H)) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
divs ['a,b'] is non empty set
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (upper_sum_set (((H + 1) (#) (#Z H)) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set (((H + 1) (#) (#Z H)) || ['a,b']))) is V11() real ext-real Element of REAL
- (integral (((H + 1) (#) (#Z H)),['a,b'])) is V11() real ext-real Element of REAL
- (integral (((H + 1) (#) (#Z H)),b,a)) is V11() real ext-real Element of REAL
(- (integral (((H + 1) (#) (#Z H)),b,a))) + ((#Z (H + 1)) . a) is V11() real ext-real Element of REAL
a is V11() real ext-real set
b is V11() real ext-real set
['a,b'] is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
H is V13() V16( NAT ) V17( PFuncs (REAL,REAL)) V18() V27( NAT , PFuncs (REAL,REAL)) Element of K6(K7(NAT,(PFuncs (REAL,REAL))))
lim (H,['a,b']) is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(lim (H,['a,b'])) | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
integral ((lim (H,['a,b'])),a,b) is V11() real ext-real Element of REAL
rseq is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
lim rseq is V11() real ext-real Element of REAL
divs ['a,b'] is non empty set
K7(NAT,(divs ['a,b'])) is set
K6(K7(NAT,(divs ['a,b']))) is set
T is V13() V16( NAT ) V17( divs ['a,b']) V18() total V27( NAT , divs ['a,b']) Element of K6(K7(NAT,(divs ['a,b'])))
delta T is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
lim (delta T) is V11() real ext-real Element of REAL
K7(['a,b'],REAL) is V40() V41() V42() set
K6(K7(['a,b'],REAL)) is set
L1 is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . L1 is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . L1) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
((H . L1) || ['a,b']) | ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
lower_sum (((H . L1) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
lim (lower_sum (((H . L1) || ['a,b']),T)) is V11() real ext-real Element of REAL
lower_integral ((H . L1) || ['a,b']) is V11() real ext-real Element of REAL
lower_sum_set ((H . L1) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (lower_sum_set ((H . L1) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (lower_sum_set ((H . L1) || ['a,b']))) is V11() real ext-real Element of REAL
upper_sum (((H . L1) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
lim (upper_sum (((H . L1) || ['a,b']),T)) is V11() real ext-real Element of REAL
upper_integral ((H . L1) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((H . L1) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((H . L1) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((H . L1) || ['a,b']))) is V11() real ext-real Element of REAL
rseq . L1 is V11() real ext-real Element of REAL
integral ((H . L1) || ['a,b']) is V11() real ext-real Element of REAL
dom (H . L1) is V50() V51() V52() Element of K6(REAL)
integral ((H . L1),a,b) is V11() real ext-real Element of REAL
integral ((H . L1),['a,b']) is V11() real ext-real Element of REAL
(lim (H,['a,b'])) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
lower_integral ((lim (H,['a,b'])) || ['a,b']) is V11() real ext-real Element of REAL
lower_sum_set ((lim (H,['a,b'])) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
K7((divs ['a,b']),REAL) is V40() V41() V42() set
K6(K7((divs ['a,b']),REAL)) is set
rng (lower_sum_set ((lim (H,['a,b'])) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (lower_sum_set ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
upper_integral ((lim (H,['a,b'])) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((lim (H,['a,b'])) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((lim (H,['a,b'])) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
b - a is V11() real ext-real set
- a is V11() real ext-real set
b + (- a) is V11() real ext-real set
K is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . K is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . K) | ['a,b'] is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
dom (H . K) is V50() V51() V52() Element of K6(REAL)
['a,b'] /\ (dom (H . K)) is V50() V51() V52() Element of K6(REAL)
r is V11() real ext-real set
dom (lim (H,['a,b'])) is V50() V51() V52() Element of K6(REAL)
['a,b'] /\ (dom (lim (H,['a,b']))) is V50() V51() V52() Element of K6(REAL)
p is set
(lim (H,['a,b'])) . p is V11() real ext-real Element of REAL
(H . K) . p is V11() real ext-real Element of REAL
((H . K) . p) - ((lim (H,['a,b'])) . p) is V11() real ext-real Element of REAL
- ((lim (H,['a,b'])) . p) is V11() real ext-real set
((H . K) . p) + (- ((lim (H,['a,b'])) . p)) is V11() real ext-real set
((H . K) . p) - (((H . K) . p) - ((lim (H,['a,b'])) . p)) is V11() real ext-real Element of REAL
- (((H . K) . p) - ((lim (H,['a,b'])) . p)) is V11() real ext-real set
((H . K) . p) + (- (((H . K) . p) - ((lim (H,['a,b'])) . p))) is V11() real ext-real set
abs ((lim (H,['a,b'])) . p) is V11() real ext-real Element of REAL
abs ((H . K) . p) is V11() real ext-real Element of REAL
abs (((H . K) . p) - ((lim (H,['a,b'])) . p)) is V11() real ext-real Element of REAL
(abs ((H . K) . p)) + (abs (((H . K) . p) - ((lim (H,['a,b'])) . p))) is V11() real ext-real Element of REAL
r + 1 is V11() real ext-real Element of REAL
((lim (H,['a,b'])) || ['a,b']) | ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_sum (((lim (H,['a,b'])) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
p is V11() real ext-real Element of REAL
p * (b - a) is V11() real ext-real Element of REAL
e is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
T . n is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V44() V46() FinSequence-like Division of ['a,b']
n is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V44() V46() FinSequence-like Division of ['a,b']
len n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
dom n is V50() V51() V52() V53() V54() V55() bounded_below Element of K6(NAT)
Seg (len n) is V50() V51() V52() V53() V54() V55() bounded_below Element of K6(NAT)
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_volume (((H . N) || ['a,b']),(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
len (upper_volume (((H . N) || ['a,b']),(T . n))) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(len n) -tuples_on REAL is non empty V21() FinSequence-membered FinSequenceSet of REAL
upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
len (upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
upper_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
(upper_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) - ((upper_sum (((H . N) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((upper_sum (((H . N) || ['a,b']),T)) . n) is V11() real ext-real set
((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) + (- ((upper_sum (((H . N) || ['a,b']),T)) . n)) is V11() real ext-real set
upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n)) is V11() real ext-real Element of REAL
Sum (upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
(upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) - ((upper_sum (((H . N) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
(upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) + (- ((upper_sum (((H . N) || ['a,b']),T)) . n)) is V11() real ext-real set
upper_sum (((H . N) || ['a,b']),(T . n)) is V11() real ext-real Element of REAL
Sum (upper_volume (((H . N) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
(upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) - (upper_sum (((H . N) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
- (upper_sum (((H . N) || ['a,b']),(T . n))) is V11() real ext-real set
(upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) + (- (upper_sum (((H . N) || ['a,b']),(T . n)))) is V11() real ext-real set
R2 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len n) FinSequence-like Element of (len n) -tuples_on REAL
H1 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len n) FinSequence-like Element of (len n) -tuples_on REAL
R2 - H1 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len n) FinSequence-like Element of (len n) -tuples_on REAL
- H1 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
- 1 is V11() real ext-real V89() set
(- 1) (#) H1 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
R2 + (- H1) is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
Sum (R2 - H1) is V11() real ext-real Element of REAL
{p} is non empty V50() V51() V52() Element of K6(REAL)
R1 is non empty V13() V16(['a,b']) V17( REAL ) V18() total V27(['a,b'], REAL ) V40() V41() V42() Element of K6(K7(['a,b'],REAL))
rng R1 is V50() V51() V52() Element of K6(REAL)
R1 | ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_volume (R1,(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
len (upper_volume (R1,(T . n))) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
vol ['a,b'] is V11() real ext-real Element of REAL
upper_bound ['a,b'] is V11() real ext-real Element of REAL
lower_bound ['a,b'] is V11() real ext-real Element of REAL
(upper_bound ['a,b']) - (lower_bound ['a,b']) is V11() real ext-real Element of REAL
- (lower_bound ['a,b']) is V11() real ext-real set
(upper_bound ['a,b']) + (- (lower_bound ['a,b'])) is V11() real ext-real set
upper_bound (rng R1) is V11() real ext-real Element of REAL
upper_sum (R1,(T . n)) is V11() real ext-real Element of REAL
Sum (upper_volume (R1,(T . n))) is V11() real ext-real Element of REAL
H1 - R2 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len n) FinSequence-like Element of (len n) -tuples_on REAL
- R2 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
(- 1) (#) R2 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
H1 + (- R2) is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
R3 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len n) FinSequence-like Element of (len n) -tuples_on REAL
i is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(H1 - R2) . i is V11() real ext-real Element of REAL
R3 . i is V11() real ext-real Element of REAL
(R2 - H1) . i is V11() real ext-real Element of REAL
divset ((T . n),i) is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
vol (divset ((T . n),i)) is V11() real ext-real Element of REAL
upper_bound (divset ((T . n),i)) is V11() real ext-real Element of REAL
lower_bound (divset ((T . n),i)) is V11() real ext-real Element of REAL
(upper_bound (divset ((T . n),i))) - (lower_bound (divset ((T . n),i))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((T . n),i))) is V11() real ext-real set
(upper_bound (divset ((T . n),i))) + (- (lower_bound (divset ((T . n),i)))) is V11() real ext-real set
((H . N) || ['a,b']) | (divset ((T . n),i)) is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
rng (((H . N) || ['a,b']) | (divset ((T . n),i))) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i)))) is V11() real ext-real Element of REAL
((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)) is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)))) is V11() real ext-real Element of REAL
(upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) - (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real Element of REAL
- (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real set
(upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) + (- (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)))))) is V11() real ext-real set
R1 | (divset ((T . n),i)) is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
rng (R1 | (divset ((T . n),i))) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (R1 | (divset ((T . n),i)))) is V11() real ext-real Element of REAL
(upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) - (upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real Element of REAL
- (upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real set
(upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) + (- (upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i)))))) is V11() real ext-real set
K7((divset ((T . n),i)),REAL) is V40() V41() V42() set
K6(K7((divset ((T . n),i)),REAL)) is set
g is set
f is non empty V13() V16( divset ((T . n),i)) V17( REAL ) V18() total V27( divset ((T . n),i), REAL ) V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
x0 is non empty V13() V16( divset ((T . n),i)) V17( REAL ) V18() total V27( divset ((T . n),i), REAL ) V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
x is set
f . x is V11() real ext-real Element of REAL
x0 . x is V11() real ext-real Element of REAL
(f . x) - (x0 . x) is V11() real ext-real Element of REAL
- (x0 . x) is V11() real ext-real set
(f . x) + (- (x0 . x)) is V11() real ext-real set
abs ((f . x) - (x0 . x)) is V11() real ext-real Element of REAL
((H . N) || ['a,b']) . x is V11() real ext-real Element of REAL
(((H . N) || ['a,b']) . x) - (x0 . x) is V11() real ext-real Element of REAL
(((H . N) || ['a,b']) . x) + (- (x0 . x)) is V11() real ext-real set
abs ((((H . N) || ['a,b']) . x) - (x0 . x)) is V11() real ext-real Element of REAL
((lim (H,['a,b'])) || ['a,b']) . x is V11() real ext-real Element of REAL
(((H . N) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x) is V11() real ext-real Element of REAL
- (((lim (H,['a,b'])) || ['a,b']) . x) is V11() real ext-real set
(((H . N) || ['a,b']) . x) + (- (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real set
abs ((((H . N) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real Element of REAL
(H . N) . x is V11() real ext-real Element of REAL
((H . N) . x) - (((lim (H,['a,b'])) || ['a,b']) . x) is V11() real ext-real Element of REAL
((H . N) . x) + (- (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real set
abs (((H . N) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real Element of REAL
(lim (H,['a,b'])) . x is V11() real ext-real Element of REAL
((H . N) . x) - ((lim (H,['a,b'])) . x) is V11() real ext-real Element of REAL
- ((lim (H,['a,b'])) . x) is V11() real ext-real set
((H . N) . x) + (- ((lim (H,['a,b'])) . x)) is V11() real ext-real set
abs (((H . N) . x) - ((lim (H,['a,b'])) . x)) is V11() real ext-real Element of REAL
((H . N) || ['a,b']) | ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
f | (divset ((T . n),i)) is V13() V16( divset ((T . n),i)) V17( REAL ) V18() V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
rng f is V50() V51() V52() Element of K6(REAL)
R1 . g is V11() real ext-real Element of REAL
(R1 | (divset ((T . n),i))) . g is V11() real ext-real Element of REAL
x0 | (divset ((T . n),i)) is V13() V16( divset ((T . n),i)) V17( REAL ) V18() V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
rng x0 is V50() V51() V52() Element of K6(REAL)
x is set
x0 . x is V11() real ext-real Element of REAL
f . x is V11() real ext-real Element of REAL
(x0 . x) - (f . x) is V11() real ext-real Element of REAL
- (f . x) is V11() real ext-real set
(x0 . x) + (- (f . x)) is V11() real ext-real set
abs ((x0 . x) - (f . x)) is V11() real ext-real Element of REAL
(f . x) - (x0 . x) is V11() real ext-real Element of REAL
- (x0 . x) is V11() real ext-real set
(f . x) + (- (x0 . x)) is V11() real ext-real set
abs ((f . x) - (x0 . x)) is V11() real ext-real Element of REAL
H1 . i is V11() real ext-real Element of REAL
R2 . i is V11() real ext-real Element of REAL
(H1 . i) - (R2 . i) is V11() real ext-real Element of REAL
- (R2 . i) is V11() real ext-real set
(H1 . i) + (- (R2 . i)) is V11() real ext-real set
(upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
(upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i is V11() real ext-real Element of REAL
((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i) is V11() real ext-real Element of REAL
- ((upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i) is V11() real ext-real set
((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((upper_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i)) is V11() real ext-real set
(upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real Element of REAL
- ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real set
((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))))) is V11() real ext-real set
((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) - (upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
(upper_bound (rng (R1 | (divset ((T . n),i))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
(R2 . i) - (H1 . i) is V11() real ext-real Element of REAL
- (H1 . i) is V11() real ext-real set
(R2 . i) + (- (H1 . i)) is V11() real ext-real set
(upper_volume (((H . N) || ['a,b']),(T . n))) . i is V11() real ext-real Element of REAL
((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((upper_volume (((H . N) || ['a,b']),(T . n))) . i) is V11() real ext-real Element of REAL
- ((upper_volume (((H . N) || ['a,b']),(T . n))) . i) is V11() real ext-real set
((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((upper_volume (((H . N) || ['a,b']),(T . n))) . i)) is V11() real ext-real set
((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real Element of REAL
- ((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real set
((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))))) is V11() real ext-real set
((upper_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) - (upper_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i)))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
i is natural V11() real ext-real V89() set
(R2 - H1) . i is V11() real ext-real Element of REAL
R3 . i is V11() real ext-real Element of REAL
Sum R3 is V11() real ext-real Element of REAL
- (p * (b - a)) is V11() real ext-real Element of REAL
- (((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) - ((upper_sum (((H . N) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((upper_sum (((H . N) || ['a,b']),T)) . n) + (- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
(upper_sum (((H . N) || ['a,b']),(T . n))) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
(upper_sum (((H . N) || ['a,b']),(T . n))) + (- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
(upper_sum (((H . N) || ['a,b']),(T . n))) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
- (upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) is V11() real ext-real set
(upper_sum (((H . N) || ['a,b']),(T . n))) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),(T . n)))) is V11() real ext-real set
Sum (H1 - R2) is V11() real ext-real Element of REAL
i is natural V11() real ext-real V89() set
(H1 - R2) . i is V11() real ext-real Element of REAL
R3 . i is V11() real ext-real Element of REAL
abs (((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(upper_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
(upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((upper_sum (((H . N) || ['a,b']),T)) . n) + (- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
abs (((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p / (b - a) is V11() real ext-real Element of REAL
(b - a) " is V11() real ext-real set
p * ((b - a) ") is V11() real ext-real set
(p / (b - a)) * (b - a) is V11() real ext-real Element of REAL
e is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(upper_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
(upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((upper_sum (((H . N) || ['a,b']),T)) . n) + (- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
abs (((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(upper_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
(upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((upper_sum (((H . N) || ['a,b']),T)) . n) + (- ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
abs (((upper_sum (((H . N) || ['a,b']),T)) . n) - ((upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real V89() set
(- 1) (#) (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V18() total V40() V41() V42() set
(- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) . n is V11() real ext-real Element of REAL
((upper_sum (((H . N) || ['a,b']),T)) . n) + ((- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) . n) is V11() real ext-real Element of REAL
abs (((upper_sum (((H . N) || ['a,b']),T)) . n) + ((- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) . n)) is V11() real ext-real Element of REAL
(upper_sum (((H . N) || ['a,b']),T)) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
((upper_sum (((H . N) || ['a,b']),T)) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . n is V11() real ext-real Element of REAL
abs (((upper_sum (((H . N) || ['a,b']),T)) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . n) is V11() real ext-real Element of REAL
(upper_sum (((H . N) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V18() total V40() V41() V42() set
(upper_sum (((H . N) || ['a,b']),T)) + (- (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V13() V16( NAT ) V18() total V40() V41() V42() set
abs ((upper_sum (((H . N) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
(abs ((upper_sum (((H . N) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . n is V11() real ext-real Element of REAL
lim ((upper_sum (((H . N) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real Element of REAL
lim (upper_sum (((H . N) || ['a,b']),T)) is V11() real ext-real Element of REAL
lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V11() real ext-real Element of REAL
(lim (upper_sum (((H . N) || ['a,b']),T))) - (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real Element of REAL
- (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real set
(lim (upper_sum (((H . N) || ['a,b']),T))) + (- (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) is V11() real ext-real set
upper_integral ((H . N) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((H . N) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((H . N) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((H . N) || ['a,b']))) is V11() real ext-real Element of REAL
(upper_integral ((H . N) || ['a,b'])) - (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real Element of REAL
(upper_integral ((H . N) || ['a,b'])) + (- (lim (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) is V11() real ext-real set
(upper_integral ((H . N) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
- (upper_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real set
(upper_integral ((H . N) || ['a,b'])) + (- (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
lim (abs ((upper_sum (((H . N) || ['a,b']),T)) - (upper_sum (((lim (H,['a,b'])) || ['a,b']),T)))) is V11() real ext-real Element of REAL
abs ((upper_integral ((H . N) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
lower_sum (((lim (H,['a,b'])) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
p is V11() real ext-real Element of REAL
p * (b - a) is V11() real ext-real Element of REAL
e is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
T . n is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V44() V46() FinSequence-like Division of ['a,b']
K is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V44() V46() FinSequence-like Division of ['a,b']
len K is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
{p} is non empty V50() V51() V52() Element of K6(REAL)
H1 is non empty V13() V16(['a,b']) V17( REAL ) V18() total V27(['a,b'], REAL ) V40() V41() V42() Element of K6(K7(['a,b'],REAL))
rng H1 is V50() V51() V52() Element of K6(REAL)
H1 | ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
lower_sum (H1,(T . n)) is V11() real ext-real Element of REAL
lower_volume (H1,(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
Sum (lower_volume (H1,(T . n))) is V11() real ext-real Element of REAL
upper_sum (H1,(T . n)) is V11() real ext-real Element of REAL
upper_volume (H1,(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
Sum (upper_volume (H1,(T . n))) is V11() real ext-real Element of REAL
lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
len (lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(len K) -tuples_on REAL is non empty V21() FinSequence-membered FinSequenceSet of REAL
lower_volume (((H . N) || ['a,b']),(T . n)) is non empty V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() FinSequence-like FinSequence of REAL
len (lower_volume (((H . N) || ['a,b']),(T . n))) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
len (lower_volume (H1,(T . n))) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
dom K is V50() V51() V52() V53() V54() V55() bounded_below Element of K6(NAT)
R1 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len K) FinSequence-like Element of (len K) -tuples_on REAL
R2 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len K) FinSequence-like Element of (len K) -tuples_on REAL
R1 - R2 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len K) FinSequence-like Element of (len K) -tuples_on REAL
- R2 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
- 1 is V11() real ext-real V89() set
(- 1) (#) R2 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
R1 + (- R2) is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
R3 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len K) FinSequence-like Element of (len K) -tuples_on REAL
R2 - R1 is V13() V16( NAT ) V17( REAL ) V18() V40() V41() V42() V64( len K) FinSequence-like Element of (len K) -tuples_on REAL
- R1 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
(- 1) (#) R1 is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
R2 + (- R1) is V13() V16( NAT ) V18() V40() V41() V42() FinSequence-like set
i is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(R1 - R2) . i is V11() real ext-real Element of REAL
R3 . i is V11() real ext-real Element of REAL
(R2 - R1) . i is V11() real ext-real Element of REAL
divset ((T . n),i) is non empty V50() V51() V52() compact closed V72() bounded_below bounded_above real-bounded V100() Element of K6(REAL)
x0 is set
H1 | (divset ((T . n),i)) is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
rng (H1 | (divset ((T . n),i))) is V50() V51() V52() Element of K6(REAL)
K7((divset ((T . n),i)),REAL) is V40() V41() V42() set
K6(K7((divset ((T . n),i)),REAL)) is set
((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)) is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
((H . N) || ['a,b']) | (divset ((T . n),i)) is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
vol (divset ((T . n),i)) is V11() real ext-real Element of REAL
upper_bound (divset ((T . n),i)) is V11() real ext-real Element of REAL
lower_bound (divset ((T . n),i)) is V11() real ext-real Element of REAL
(upper_bound (divset ((T . n),i))) - (lower_bound (divset ((T . n),i))) is V11() real ext-real Element of REAL
- (lower_bound (divset ((T . n),i))) is V11() real ext-real set
(upper_bound (divset ((T . n),i))) + (- (lower_bound (divset ((T . n),i)))) is V11() real ext-real set
H1 . x0 is V11() real ext-real Element of REAL
(H1 | (divset ((T . n),i))) . x0 is V11() real ext-real Element of REAL
lower_bound (rng (H1 | (divset ((T . n),i)))) is V11() real ext-real Element of REAL
x is set
f is non empty V13() V16( divset ((T . n),i)) V17( REAL ) V18() total V27( divset ((T . n),i), REAL ) V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
f . x is V11() real ext-real Element of REAL
g is non empty V13() V16( divset ((T . n),i)) V17( REAL ) V18() total V27( divset ((T . n),i), REAL ) V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
g . x is V11() real ext-real Element of REAL
(f . x) - (g . x) is V11() real ext-real Element of REAL
- (g . x) is V11() real ext-real set
(f . x) + (- (g . x)) is V11() real ext-real set
abs ((f . x) - (g . x)) is V11() real ext-real Element of REAL
((H . N) || ['a,b']) . x is V11() real ext-real Element of REAL
(((H . N) || ['a,b']) . x) - (g . x) is V11() real ext-real Element of REAL
(((H . N) || ['a,b']) . x) + (- (g . x)) is V11() real ext-real set
abs ((((H . N) || ['a,b']) . x) - (g . x)) is V11() real ext-real Element of REAL
((lim (H,['a,b'])) || ['a,b']) . x is V11() real ext-real Element of REAL
(((H . N) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x) is V11() real ext-real Element of REAL
- (((lim (H,['a,b'])) || ['a,b']) . x) is V11() real ext-real set
(((H . N) || ['a,b']) . x) + (- (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real set
abs ((((H . N) || ['a,b']) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real Element of REAL
(H . N) . x is V11() real ext-real Element of REAL
((H . N) . x) - (((lim (H,['a,b'])) || ['a,b']) . x) is V11() real ext-real Element of REAL
((H . N) . x) + (- (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real set
abs (((H . N) . x) - (((lim (H,['a,b'])) || ['a,b']) . x)) is V11() real ext-real Element of REAL
(lim (H,['a,b'])) . x is V11() real ext-real Element of REAL
((H . N) . x) - ((lim (H,['a,b'])) . x) is V11() real ext-real Element of REAL
- ((lim (H,['a,b'])) . x) is V11() real ext-real set
((H . N) . x) + (- ((lim (H,['a,b'])) . x)) is V11() real ext-real set
abs (((H . N) . x) - ((lim (H,['a,b'])) . x)) is V11() real ext-real Element of REAL
R2 . i is V11() real ext-real Element of REAL
R1 . i is V11() real ext-real Element of REAL
(R2 . i) - (R1 . i) is V11() real ext-real Element of REAL
- (R1 . i) is V11() real ext-real set
(R2 . i) + (- (R1 . i)) is V11() real ext-real set
rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)))) is V11() real ext-real Element of REAL
(lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
(lower_volume (((H . N) || ['a,b']),(T . n))) . i is V11() real ext-real Element of REAL
((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((lower_volume (((H . N) || ['a,b']),(T . n))) . i) is V11() real ext-real Element of REAL
- ((lower_volume (((H . N) || ['a,b']),(T . n))) . i) is V11() real ext-real set
((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((lower_volume (((H . N) || ['a,b']),(T . n))) . i)) is V11() real ext-real set
rng (((H . N) || ['a,b']) | (divset ((T . n),i))) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i)))) is V11() real ext-real Element of REAL
(lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real Element of REAL
- ((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real set
((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))))) is V11() real ext-real set
(lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) - (lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real Element of REAL
- (lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real set
(lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) + (- (lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i)))))) is V11() real ext-real set
((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) - (lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i)))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
(R1 . i) - (R2 . i) is V11() real ext-real Element of REAL
- (R2 . i) is V11() real ext-real set
(R1 . i) + (- (R2 . i)) is V11() real ext-real set
(lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i is V11() real ext-real Element of REAL
((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i) is V11() real ext-real Element of REAL
- ((lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i) is V11() real ext-real set
((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) . i)) is V11() real ext-real set
((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) - ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real Element of REAL
- ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) is V11() real ext-real set
((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i)))) + (- ((lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) * (vol (divset ((T . n),i))))) is V11() real ext-real set
(lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) - (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real Element of REAL
- (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i))))) is V11() real ext-real set
(lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) + (- (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)))))) is V11() real ext-real set
((lower_bound (rng (((H . N) || ['a,b']) | (divset ((T . n),i))))) - (lower_bound (rng (((lim (H,['a,b'])) || ['a,b']) | (divset ((T . n),i)))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
((H . N) || ['a,b']) | ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
f | (divset ((T . n),i)) is V13() V16( divset ((T . n),i)) V17( REAL ) V18() V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
rng f is V50() V51() V52() Element of K6(REAL)
g | (divset ((T . n),i)) is V13() V16( divset ((T . n),i)) V17( REAL ) V18() V40() V41() V42() Element of K6(K7((divset ((T . n),i)),REAL))
rng g is V50() V51() V52() Element of K6(REAL)
(lower_bound (rng (H1 | (divset ((T . n),i))))) * (vol (divset ((T . n),i))) is V11() real ext-real Element of REAL
x is set
f . x is V11() real ext-real Element of REAL
g . x is V11() real ext-real Element of REAL
(f . x) - (g . x) is V11() real ext-real Element of REAL
- (g . x) is V11() real ext-real set
(f . x) + (- (g . x)) is V11() real ext-real set
abs ((f . x) - (g . x)) is V11() real ext-real Element of REAL
(g . x) - (f . x) is V11() real ext-real Element of REAL
- (f . x) is V11() real ext-real set
(g . x) + (- (f . x)) is V11() real ext-real set
abs ((g . x) - (f . x)) is V11() real ext-real Element of REAL
lower_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
(lower_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
(lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((lower_sum (((H . N) || ['a,b']),T)) . n) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((lower_sum (((H . N) || ['a,b']),T)) . n) + (- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
lower_sum (((H . N) || ['a,b']),(T . n)) is V11() real ext-real Element of REAL
Sum (lower_volume (((H . N) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
(lower_sum (((H . N) || ['a,b']),(T . n))) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
(lower_sum (((H . N) || ['a,b']),(T . n))) + (- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n)) is V11() real ext-real Element of REAL
Sum (lower_volume (((lim (H,['a,b'])) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
(lower_sum (((H . N) || ['a,b']),(T . n))) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
- (lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) is V11() real ext-real set
(lower_sum (((H . N) || ['a,b']),(T . n))) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n)))) is V11() real ext-real set
Sum (R1 - R2) is V11() real ext-real Element of REAL
vol ['a,b'] is V11() real ext-real Element of REAL
upper_bound ['a,b'] is V11() real ext-real Element of REAL
lower_bound ['a,b'] is V11() real ext-real Element of REAL
(upper_bound ['a,b']) - (lower_bound ['a,b']) is V11() real ext-real Element of REAL
- (lower_bound ['a,b']) is V11() real ext-real set
(upper_bound ['a,b']) + (- (lower_bound ['a,b'])) is V11() real ext-real set
upper_bound (rng H1) is V11() real ext-real Element of REAL
((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) - ((lower_sum (((H . N) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((lower_sum (((H . N) || ['a,b']),T)) . n) is V11() real ext-real set
((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) + (- ((lower_sum (((H . N) || ['a,b']),T)) . n)) is V11() real ext-real set
(lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) - ((lower_sum (((H . N) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
(lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) + (- ((lower_sum (((H . N) || ['a,b']),T)) . n)) is V11() real ext-real set
(lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) - (lower_sum (((H . N) || ['a,b']),(T . n))) is V11() real ext-real Element of REAL
- (lower_sum (((H . N) || ['a,b']),(T . n))) is V11() real ext-real set
(lower_sum (((lim (H,['a,b'])) || ['a,b']),(T . n))) + (- (lower_sum (((H . N) || ['a,b']),(T . n)))) is V11() real ext-real set
Sum (R2 - R1) is V11() real ext-real Element of REAL
Seg (len K) is V50() V51() V52() V53() V54() V55() bounded_below Element of K6(NAT)
i is natural V11() real ext-real V89() set
(R2 - R1) . i is V11() real ext-real Element of REAL
R3 . i is V11() real ext-real Element of REAL
Sum R3 is V11() real ext-real Element of REAL
- (p * (b - a)) is V11() real ext-real Element of REAL
- (((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) - ((lower_sum (((H . N) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
i is natural V11() real ext-real V89() set
(R1 - R2) . i is V11() real ext-real Element of REAL
R3 . i is V11() real ext-real Element of REAL
abs (((lower_sum (((H . N) || ['a,b']),T)) . n) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p / (b - a) is V11() real ext-real Element of REAL
(b - a) " is V11() real ext-real set
p * ((b - a) ") is V11() real ext-real set
(p / (b - a)) * (b - a) is V11() real ext-real Element of REAL
e is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
lower_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(lower_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
(lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((lower_sum (((H . N) || ['a,b']),T)) . n) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((lower_sum (((H . N) || ['a,b']),T)) . n) + (- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
abs (((lower_sum (((H . N) || ['a,b']),T)) . n) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
e is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . N is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . N) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
lower_sum (((H . N) || ['a,b']),T) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
(lower_sum (((H . N) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
(lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n is V11() real ext-real Element of REAL
((lower_sum (((H . N) || ['a,b']),T)) . n) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real Element of REAL
- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n) is V11() real ext-real set
((lower_sum (((H . N) || ['a,b']),T)) . n) + (- ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real set
abs (((lower_sum (((H . N) || ['a,b']),T)) . n) - ((lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) . n)) is V11() real ext-real Element of REAL
- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
- 1 is V11() real ext-real V89() set
(- 1) (#) (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V18() total V40() V41() V42() set
(- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) . n is V11() real ext-real Element of REAL
((lower_sum (((H . N) || ['a,b']),T)) . n) + ((- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) . n) is V11() real ext-real Element of REAL
abs (((lower_sum (((H . N) || ['a,b']),T)) . n) + ((- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) . n)) is V11() real ext-real Element of REAL
(lower_sum (((H . N) || ['a,b']),T)) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
((lower_sum (((H . N) || ['a,b']),T)) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . n is V11() real ext-real Element of REAL
abs (((lower_sum (((H . N) || ['a,b']),T)) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . n) is V11() real ext-real Element of REAL
(lower_sum (((H . N) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V13() V16( NAT ) V18() total V40() V41() V42() set
(lower_sum (((H . N) || ['a,b']),T)) + (- (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V13() V16( NAT ) V18() total V40() V41() V42() set
abs ((lower_sum (((H . N) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V13() V16( NAT ) V17( REAL ) V18() total V27( NAT , REAL ) V40() V41() V42() Element of K6(K7(NAT,REAL))
(abs ((lower_sum (((H . N) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) . n is V11() real ext-real Element of REAL
lim ((lower_sum (((H . N) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real Element of REAL
lim (lower_sum (((H . N) || ['a,b']),T)) is V11() real ext-real Element of REAL
lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)) is V11() real ext-real Element of REAL
(lim (lower_sum (((H . N) || ['a,b']),T))) - (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real Element of REAL
- (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real set
(lim (lower_sum (((H . N) || ['a,b']),T))) + (- (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) is V11() real ext-real set
lower_integral ((H . N) || ['a,b']) is V11() real ext-real Element of REAL
lower_sum_set ((H . N) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (lower_sum_set ((H . N) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (lower_sum_set ((H . N) || ['a,b']))) is V11() real ext-real Element of REAL
(lower_integral ((H . N) || ['a,b'])) - (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T))) is V11() real ext-real Element of REAL
(lower_integral ((H . N) || ['a,b'])) + (- (lim (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) is V11() real ext-real set
(lower_integral ((H . N) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
- (lower_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real set
(lower_integral ((H . N) || ['a,b'])) + (- (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
lim (abs ((lower_sum (((H . N) || ['a,b']),T)) - (lower_sum (((lim (H,['a,b'])) || ['a,b']),T)))) is V11() real ext-real Element of REAL
abs ((lower_integral ((H . N) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
p is V11() real ext-real Element of REAL
p / 2 is V11() real ext-real Element of REAL
2 " is V11() real ext-real positive set
p * (2 ") is V11() real ext-real set
(p / 2) / 2 is V11() real ext-real Element of REAL
(p / 2) * (2 ") is V11() real ext-real set
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
max (N,n) is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . n is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . n) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_integral ((H . n) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((H . n) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((H . n) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((H . n) || ['a,b']))) is V11() real ext-real Element of REAL
lower_integral ((H . n) || ['a,b']) is V11() real ext-real Element of REAL
lower_sum_set ((H . n) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (lower_sum_set ((H . n) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
upper_bound (rng (lower_sum_set ((H . n) || ['a,b']))) is V11() real ext-real Element of REAL
(lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
- (lower_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real set
(lower_integral ((H . n) || ['a,b'])) + (- (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
abs ((lower_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
(upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
(upper_integral ((H . n) || ['a,b'])) + (- (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
(upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
- (upper_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real set
(upper_integral ((H . n) || ['a,b'])) + (- (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) - ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
- ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) + (- ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])))) is V11() real ext-real set
(lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
(lower_integral ((lim (H,['a,b'])) || ['a,b'])) + (- (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
abs ((lower_integral ((lim (H,['a,b'])) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
(abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])))) + (abs ((upper_integral ((H . n) || ['a,b'])) - (lower_integral ((lim (H,['a,b'])) || ['a,b'])))) is V11() real ext-real Element of REAL
((p / 2) / 2) + ((p / 2) / 2) is V11() real ext-real Element of REAL
p is V11() real ext-real set
p / 2 is V11() real ext-real Element of REAL
p * (2 ") is V11() real ext-real set
N is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
n is natural V11() real ext-real V50() V51() V52() V53() V54() V55() V89() V90() bounded_below Element of NAT
H . n is V13() V16( REAL ) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(REAL,REAL))
(H . n) || ['a,b'] is V13() V16(['a,b']) V17( REAL ) V18() V40() V41() V42() Element of K6(K7(['a,b'],REAL))
upper_integral ((H . n) || ['a,b']) is V11() real ext-real Element of REAL
upper_sum_set ((H . n) || ['a,b']) is non empty V13() V16( divs ['a,b']) V17( REAL ) V18() total V27( divs ['a,b'], REAL ) V40() V41() V42() Element of K6(K7((divs ['a,b']),REAL))
rng (upper_sum_set ((H . n) || ['a,b'])) is V50() V51() V52() Element of K6(REAL)
lower_bound (rng (upper_sum_set ((H . n) || ['a,b']))) is V11() real ext-real Element of REAL
integral ((H . n) || ['a,b']) is V11() real ext-real Element of REAL
rseq . n is V11() real ext-real Element of REAL
integral ((lim (H,['a,b'])),['a,b']) is V11() real ext-real Element of REAL
integral ((lim (H,['a,b'])) || ['a,b']) is V11() real ext-real Element of REAL
(upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b'])) is V11() real ext-real Element of REAL
(upper_integral ((H . n) || ['a,b'])) + (- (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real set
abs ((upper_integral ((H . n) || ['a,b'])) - (upper_integral ((lim (H,['a,b'])) || ['a,b']))) is V11() real ext-real Element of REAL
(rseq . n) - (integral ((lim (H,['a,b'])),a,b)) is V11() real ext-real Element of REAL
- (integral ((lim (H,['a,b'])),a,b)) is V11() real ext-real set
(rseq . n) + (- (integral ((lim (H,['a,b'])),a,b))) is V11() real ext-real set
abs ((rseq . n) - (integral ((lim (H,['a,b'])),a,b))) is V11() real ext-real Element of REAL