:: 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(