:: INTEGR10 semantic presentation

REAL is non empty V55() V56() V57() V61() V68() set
NAT is V55() V56() V57() V58() V59() V60() V61() Element of K6(REAL)
K6(REAL) is set
K7(REAL,REAL) is V41() V42() V43() set
K6(K7(REAL,REAL)) is set
ExtREAL is non empty V56() set
COMPLEX is non empty V55() V61() V68() set
omega is V55() V56() V57() V58() V59() V60() V61() set
K6(omega) is set
K6(NAT) is set
RAT is non empty V55() V56() V57() V58() V61() V68() set
INT is non empty V55() V56() V57() V58() V59() V61() V68() set
K7(NAT,REAL) is V41() V42() V43() set
K6(K7(NAT,REAL)) is set
K7(NAT,COMPLEX) is V41() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V41() set
K6(K7(COMPLEX,COMPLEX)) is set
0 is empty ordinal natural V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() V66() V79() Element of NAT
{} is empty V55() V56() V57() V58() V59() V60() V61() set
2 is non empty ordinal natural V11() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V66() V79() Element of NAT
exp_R is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() continuous Element of K6(K7(REAL,REAL))
-infty is non empty non real ext-real non positive negative set
+infty is non empty non real ext-real positive non negative set
dom exp_R is V55() V56() V57() Element of K6(REAL)
a is V11() real ext-real set
f is V11() real ext-real set
Intf is V11() real ext-real set
F is V11() real ext-real set
Intf / F is V11() real ext-real set
F " is V11() real ext-real set
Intf * (F ") is V11() real ext-real set
a - (Intf / F) is V11() real ext-real set
- (Intf / F) is V11() real ext-real set
a + (- (Intf / F)) is V11() real ext-real set
max (f,(a - (Intf / F))) is V11() real ext-real set
s is V11() real ext-real set
M0 is V11() real ext-real Element of REAL
a - M0 is V11() real ext-real Element of REAL
- M0 is V11() real ext-real set
a + (- M0) is V11() real ext-real set
(a - M0) * F is V11() real ext-real Element of REAL
M0 - (Intf / F) is V11() real ext-real Element of REAL
M0 + (- (Intf / F)) is V11() real ext-real set
M0 - (M0 - (Intf / F)) is V11() real ext-real Element of REAL
- (M0 - (Intf / F)) is V11() real ext-real set
M0 + (- (M0 - (Intf / F))) is V11() real ext-real set
(a - (Intf / F)) - (M0 - (Intf / F)) is V11() real ext-real Element of REAL
(a - (Intf / F)) + (- (M0 - (Intf / F))) is V11() real ext-real set
1 is non empty ordinal natural V11() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V66() V79() Element of NAT
(a - M0) * 1 is V11() real ext-real Element of REAL
Intf / 1 is V11() real ext-real Element of REAL
1 " is non empty V11() real ext-real positive non negative set
Intf * (1 ") is V11() real ext-real set
a is V11() real ext-real set
f is V11() real ext-real set
Intf is V11() real ext-real set
F is V11() real ext-real set
- f is V11() real ext-real set
- a is V11() real ext-real set
s is V11() real ext-real Element of REAL
(- f) - s is V11() real ext-real Element of REAL
- s is V11() real ext-real set
(- f) + (- s) is V11() real ext-real set
((- f) - s) * F is V11() real ext-real Element of REAL
- s is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
s - f is V11() real ext-real Element of REAL
s + (- f) is V11() real ext-real set
(s - f) * F is V11() real ext-real Element of REAL
- (- a) is V11() real ext-real set
- (- f) is V11() real ext-real set
f is V11() real ext-real Element of REAL
exp_R . f is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
exp_R . a is V11() real ext-real Element of REAL
(exp_R . f) - (exp_R . a) is V11() real ext-real Element of REAL
- (exp_R . a) is V11() real ext-real set
(exp_R . f) + (- (exp_R . a)) is V11() real ext-real set
integral (exp_R,a,f) is V11() real ext-real Element of REAL
min (a,f) is V11() real ext-real set
max (a,f) is V11() real ext-real set
[.(min (a,f)),(max (a,f)).] is V55() V56() V57() Element of K6(REAL)
exp_R | REAL is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() continuous Element of K6(K7(REAL,REAL))
exp_R . (max (a,f)) is V11() real ext-real Element of REAL
integral (exp_R,(min (a,f)),(max (a,f))) is V11() real ext-real Element of REAL
exp_R . (min (a,f)) is V11() real ext-real Element of REAL
(integral (exp_R,(min (a,f)),(max (a,f)))) + (exp_R . (min (a,f))) is V11() real ext-real Element of REAL
['f,a'] is non empty V55() V56() V57() V63() Element of K6(REAL)
integral (exp_R,['f,a']) is V11() real ext-real Element of REAL
- (integral (exp_R,['f,a'])) is V11() real ext-real Element of REAL
- (integral (exp_R,a,f)) is V11() real ext-real Element of REAL
(- (integral (exp_R,a,f))) + (exp_R . f) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
[.a,Intf.[ is V55() V56() V57() Element of K6(REAL)
F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom F is V55() V56() V57() Element of K6(REAL)
lim_left (F,Intf) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_left (s,Intf) is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_left (s,Intf) is V11() real ext-real Element of REAL
M0 is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom M0 is V55() V56() V57() Element of K6(REAL)
lim_left (M0,Intf) is V11() real ext-real Element of REAL
M0 is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom M0 is V55() V56() V57() Element of K6(REAL)
lim_left (M0,Intf) is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
s . M is V11() real ext-real Element of REAL
integral (f,a,M) is V11() real ext-real Element of REAL
M0 . M is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
].a,Intf.] is V55() V56() V57() Element of K6(REAL)
F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom F is V55() V56() V57() Element of K6(REAL)
lim_right (F,a) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_right (s,a) is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_right (s,a) is V11() real ext-real Element of REAL
M0 is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom M0 is V55() V56() V57() Element of K6(REAL)
lim_right (M0,a) is V11() real ext-real Element of REAL
M0 is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom M0 is V55() V56() V57() Element of K6(REAL)
lim_right (M0,a) is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
s . M is V11() real ext-real Element of REAL
integral (f,M,Intf) is V11() real ext-real Element of REAL
M0 . M is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a is V11() real ext-real set
right_closed_halfline a is V55() V56() V57() Element of K6(REAL)
K141(a,+infty) is set
Intf is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom Intf is V55() V56() V57() Element of K6(REAL)
lim_in+infty Intf is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in+infty s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in+infty s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in+infty s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in+infty s is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
s . M0 is V11() real ext-real Element of REAL
integral (f,a,M0) is V11() real ext-real Element of REAL
s . M0 is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a is V11() real ext-real set
left_closed_halfline a is V55() V56() V57() Element of K6(REAL)
K142(-infty,a) is set
Intf is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom Intf is V55() V56() V57() Element of K6(REAL)
lim_in-infty Intf is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in-infty s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in-infty s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in-infty s is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in-infty s is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
s . M0 is V11() real ext-real Element of REAL
integral (f,M0,a) is V11() real ext-real Element of REAL
s . M0 is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(f,0) is V11() real ext-real Element of REAL
(f,0) is V11() real ext-real Element of REAL
(f,0) + (f,0) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
f + a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
F is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
['Intf,F'] is non empty V55() V56() V57() V63() Element of K6(REAL)
((f + a),Intf,F) is V11() real ext-real Element of REAL
(f,Intf,F) is V11() real ext-real Element of REAL
(a,Intf,F) is V11() real ext-real Element of REAL
(f,Intf,F) + (a,Intf,F) is V11() real ext-real Element of REAL
[.Intf,F.[ is V55() V56() V57() Element of K6(REAL)
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_left (s,F) is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_left (s,F) is V11() real ext-real Element of REAL
s + s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (s + s) is V55() V56() V57() Element of K6(REAL)
[.Intf,F.] is V55() V56() V57() Element of K6(REAL)
(dom s) /\ (dom s) is V55() V56() V57() Element of K6(REAL)
M is V11() real ext-real Element of REAL
(s + s) . M is V11() real ext-real Element of REAL
integral ((f + a),Intf,M) is V11() real ext-real Element of REAL
[.Intf,M.] is V55() V56() V57() Element of K6(REAL)
['Intf,M'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['Intf,M'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a | ['Intf,M'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s . M is V11() real ext-real Element of REAL
s . M is V11() real ext-real Element of REAL
(s . M) + (s . M) is V11() real ext-real Element of REAL
integral (f,Intf,M) is V11() real ext-real Element of REAL
(integral (f,Intf,M)) + (s . M) is V11() real ext-real Element of REAL
integral (a,Intf,M) is V11() real ext-real Element of REAL
(integral (f,Intf,M)) + (integral (a,Intf,M)) is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
Intf - Intf is V11() real ext-real Element of REAL
- Intf is V11() real ext-real set
Intf + (- Intf) is V11() real ext-real set
M - Intf is V11() real ext-real Element of REAL
M + (- Intf) is V11() real ext-real set
F - M is V11() real ext-real Element of REAL
- M is V11() real ext-real set
F + (- M) is V11() real ext-real set
(F - M) / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
(F - M) * (2 ") is V11() real ext-real set
M + ((F - M) / 2) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
(F - M) + M is V11() real ext-real Element of REAL
((F - M) / 2) + M is V11() real ext-real Element of REAL
r - 0 is V11() real ext-real Element of REAL
- 0 is empty V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() set
r + (- 0) is V11() real ext-real set
M - (M - Intf) is V11() real ext-real Element of REAL
- (M - Intf) is V11() real ext-real set
M + (- (M - Intf)) is V11() real ext-real set
M is V11() real ext-real Element of REAL
['Intf,M'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(f + a) | ['Intf,M'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.Intf,M.] is V55() V56() V57() Element of K6(REAL)
[.Intf,F.] is V55() V56() V57() Element of K6(REAL)
f | ['Intf,M'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a | ['Intf,M'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
['Intf,M'] /\ ['Intf,M'] is V55() V56() V57() Element of K6(REAL)
(f + a) | (['Intf,M'] /\ ['Intf,M']) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_left ((s + s),F) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
Intf is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
['a,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(f,a,Intf) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
F (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((F (#) f),a,Intf) is V11() real ext-real Element of REAL
F * (f,a,Intf) is V11() real ext-real Element of REAL
[.a,Intf.[ is V55() V56() V57() Element of K6(REAL)
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_left (s,Intf) is V11() real ext-real Element of REAL
F (#) s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (F (#) s) is V55() V56() V57() Element of K6(REAL)
[.a,Intf.] is V55() V56() V57() Element of K6(REAL)
M0 is V11() real ext-real Element of REAL
(F (#) s) . M0 is V11() real ext-real Element of REAL
integral ((F (#) f),a,M0) is V11() real ext-real Element of REAL
['a,M0'] is non empty V55() V56() V57() V63() Element of K6(REAL)
[.a,M0.] is V55() V56() V57() Element of K6(REAL)
f | ['a,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s . M0 is V11() real ext-real Element of REAL
F * (s . M0) is V11() real ext-real Element of REAL
integral (f,a,M0) is V11() real ext-real Element of REAL
F * (integral (f,a,M0)) is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
['a,M0'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(F (#) f) | ['a,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.a,M0.] is V55() V56() V57() Element of K6(REAL)
[.a,Intf.] is V55() V56() V57() Element of K6(REAL)
f | ['a,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_left ((F (#) s),Intf) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
F (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s is V11() real ext-real Element of REAL
s (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((s (#) f),a,Intf) is V11() real ext-real Element of REAL
s * (f,a,Intf) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
f + a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
F is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
['Intf,F'] is non empty V55() V56() V57() V63() Element of K6(REAL)
((f + a),Intf,F) is V11() real ext-real Element of REAL
(f,Intf,F) is V11() real ext-real Element of REAL
(a,Intf,F) is V11() real ext-real Element of REAL
(f,Intf,F) + (a,Intf,F) is V11() real ext-real Element of REAL
].Intf,F.] is V55() V56() V57() Element of K6(REAL)
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_right (s,Intf) is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_right (s,Intf) is V11() real ext-real Element of REAL
s + s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (s + s) is V55() V56() V57() Element of K6(REAL)
[.Intf,F.] is V55() V56() V57() Element of K6(REAL)
(dom s) /\ (dom s) is V55() V56() V57() Element of K6(REAL)
M is V11() real ext-real Element of REAL
(s + s) . M is V11() real ext-real Element of REAL
integral ((f + a),M,F) is V11() real ext-real Element of REAL
[.M,F.] is V55() V56() V57() Element of K6(REAL)
['M,F'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['M,F'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a | ['M,F'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s . M is V11() real ext-real Element of REAL
s . M is V11() real ext-real Element of REAL
(s . M) + (s . M) is V11() real ext-real Element of REAL
integral (f,M,F) is V11() real ext-real Element of REAL
(integral (f,M,F)) + (s . M) is V11() real ext-real Element of REAL
integral (a,M,F) is V11() real ext-real Element of REAL
(integral (f,M,F)) + (integral (a,M,F)) is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
M - Intf is V11() real ext-real Element of REAL
- Intf is V11() real ext-real set
M + (- Intf) is V11() real ext-real set
(M - Intf) / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
(M - Intf) * (2 ") is V11() real ext-real set
M - ((M - Intf) / 2) is V11() real ext-real Element of REAL
- ((M - Intf) / 2) is V11() real ext-real set
M + (- ((M - Intf) / 2)) is V11() real ext-real set
r is V11() real ext-real Element of REAL
Intf - ((M - Intf) / 2) is V11() real ext-real Element of REAL
Intf + (- ((M - Intf) / 2)) is V11() real ext-real set
(M - Intf) + (Intf - ((M - Intf) / 2)) is V11() real ext-real Element of REAL
((M - Intf) / 2) + (Intf - ((M - Intf) / 2)) is V11() real ext-real Element of REAL
F - 0 is V11() real ext-real Element of REAL
- 0 is empty V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() set
F + (- 0) is V11() real ext-real set
M is V11() real ext-real Element of REAL
['M,F'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(f + a) | ['M,F'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.M,F.] is V55() V56() V57() Element of K6(REAL)
[.Intf,F.] is V55() V56() V57() Element of K6(REAL)
f | ['M,F'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a | ['M,F'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
['M,F'] /\ ['M,F'] is V55() V56() V57() Element of K6(REAL)
(f + a) | (['M,F'] /\ ['M,F']) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_right ((s + s),Intf) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
Intf is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
['a,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(f,a,Intf) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
F (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((F (#) f),a,Intf) is V11() real ext-real Element of REAL
F * (f,a,Intf) is V11() real ext-real Element of REAL
].a,Intf.] is V55() V56() V57() Element of K6(REAL)
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_right (s,a) is V11() real ext-real Element of REAL
F (#) s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (F (#) s) is V55() V56() V57() Element of K6(REAL)
[.a,Intf.] is V55() V56() V57() Element of K6(REAL)
M0 is V11() real ext-real Element of REAL
(F (#) s) . M0 is V11() real ext-real Element of REAL
integral ((F (#) f),M0,Intf) is V11() real ext-real Element of REAL
[.M0,Intf.] is V55() V56() V57() Element of K6(REAL)
['M0,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s . M0 is V11() real ext-real Element of REAL
F * (s . M0) is V11() real ext-real Element of REAL
integral (f,M0,Intf) is V11() real ext-real Element of REAL
F * (integral (f,M0,Intf)) is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
['M0,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(F (#) f) | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.M0,Intf.] is V55() V56() V57() Element of K6(REAL)
[.a,Intf.] is V55() V56() V57() Element of K6(REAL)
f | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_right ((F (#) s),a) is V11() real ext-real Element of REAL
F is V11() real ext-real Element of REAL
F (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s is V11() real ext-real Element of REAL
s (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((s (#) f),a,Intf) is V11() real ext-real Element of REAL
s * (f,a,Intf) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
f + a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
Intf is V11() real ext-real set
right_closed_halfline Intf is V55() V56() V57() Element of K6(REAL)
K141(Intf,+infty) is set
((f + a),Intf) is V11() real ext-real Element of REAL
(f,Intf) is V11() real ext-real Element of REAL
(a,Intf) is V11() real ext-real Element of REAL
(f,Intf) + (a,Intf) is V11() real ext-real Element of REAL
F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom F is V55() V56() V57() Element of K6(REAL)
lim_in+infty F is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in+infty s is V11() real ext-real Element of REAL
s + F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (s + F) is V55() V56() V57() Element of K6(REAL)
(dom s) /\ (dom F) is V55() V56() V57() Element of K6(REAL)
M0 is V11() real ext-real Element of REAL
(s + F) . M0 is V11() real ext-real Element of REAL
integral ((f + a),Intf,M0) is V11() real ext-real Element of REAL
['Intf,M0'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['Intf,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.Intf,M0.] is V55() V56() V57() Element of K6(REAL)
a | ['Intf,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s . M0 is V11() real ext-real Element of REAL
F . M0 is V11() real ext-real Element of REAL
(s . M0) + (F . M0) is V11() real ext-real Element of REAL
integral (f,Intf,M0) is V11() real ext-real Element of REAL
(integral (f,Intf,M0)) + (F . M0) is V11() real ext-real Element of REAL
integral (a,Intf,M0) is V11() real ext-real Element of REAL
(integral (f,Intf,M0)) + (integral (a,Intf,M0)) is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
1 is non empty ordinal natural V11() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V66() V79() Element of NAT
M0 + 1 is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
M0 + 0 is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
['Intf,M0'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(f + a) | ['Intf,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.Intf,M0.] is V55() V56() V57() Element of K6(REAL)
f | ['Intf,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a | ['Intf,M0'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
['Intf,M0'] /\ ['Intf,M0'] is V55() V56() V57() Element of K6(REAL)
(f + a) | (['Intf,M0'] /\ ['Intf,M0']) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_in+infty (s + F) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V11() real ext-real set
right_closed_halfline a is V55() V56() V57() Element of K6(REAL)
K141(a,+infty) is set
(f,a) is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
Intf (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((Intf (#) f),a) is V11() real ext-real Element of REAL
Intf * (f,a) is V11() real ext-real Element of REAL
F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom F is V55() V56() V57() Element of K6(REAL)
lim_in+infty F is V11() real ext-real Element of REAL
Intf (#) F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (Intf (#) F) is V55() V56() V57() Element of K6(REAL)
s is V11() real ext-real Element of REAL
(Intf (#) F) . s is V11() real ext-real Element of REAL
integral ((Intf (#) f),a,s) is V11() real ext-real Element of REAL
['a,s'] is non empty V55() V56() V57() V63() Element of K6(REAL)
[.a,s.] is V55() V56() V57() Element of K6(REAL)
f | ['a,s'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
F . s is V11() real ext-real Element of REAL
Intf * (F . s) is V11() real ext-real Element of REAL
integral (f,a,s) is V11() real ext-real Element of REAL
Intf * (integral (f,a,s)) is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
['a,s'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(Intf (#) f) | ['a,s'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.a,s.] is V55() V56() V57() Element of K6(REAL)
f | ['a,s'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_in+infty (Intf (#) F) is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
Intf (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
F is V11() real ext-real Element of REAL
F (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((F (#) f),a) is V11() real ext-real Element of REAL
F * (f,a) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
f + a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
Intf is V11() real ext-real set
left_closed_halfline Intf is V55() V56() V57() Element of K6(REAL)
K142(-infty,Intf) is set
((f + a),Intf) is V11() real ext-real Element of REAL
(f,Intf) is V11() real ext-real Element of REAL
(a,Intf) is V11() real ext-real Element of REAL
(f,Intf) + (a,Intf) is V11() real ext-real Element of REAL
F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom F is V55() V56() V57() Element of K6(REAL)
lim_in-infty F is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
lim_in-infty s is V11() real ext-real Element of REAL
s + F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (s + F) is V55() V56() V57() Element of K6(REAL)
(dom s) /\ (dom F) is V55() V56() V57() Element of K6(REAL)
M0 is V11() real ext-real Element of REAL
(s + F) . M0 is V11() real ext-real Element of REAL
integral ((f + a),M0,Intf) is V11() real ext-real Element of REAL
['M0,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.M0,Intf.] is V55() V56() V57() Element of K6(REAL)
a | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
s . M0 is V11() real ext-real Element of REAL
F . M0 is V11() real ext-real Element of REAL
(s . M0) + (F . M0) is V11() real ext-real Element of REAL
integral (f,M0,Intf) is V11() real ext-real Element of REAL
(integral (f,M0,Intf)) + (F . M0) is V11() real ext-real Element of REAL
integral (a,M0,Intf) is V11() real ext-real Element of REAL
(integral (f,M0,Intf)) + (integral (a,M0,Intf)) is V11() real ext-real Element of REAL
M0 is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
1 is non empty ordinal natural V11() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V66() V79() Element of NAT
M0 - 1 is V11() real ext-real Element of REAL
- 1 is V11() real ext-real non positive set
M0 + (- 1) is V11() real ext-real set
M is V11() real ext-real Element of REAL
M0 - 0 is V11() real ext-real Element of REAL
- 0 is empty V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() set
M0 + (- 0) is V11() real ext-real set
M0 is V11() real ext-real Element of REAL
['M0,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(f + a) | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.M0,Intf.] is V55() V56() V57() Element of K6(REAL)
f | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a | ['M0,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
['M0,Intf'] /\ ['M0,Intf'] is V55() V56() V57() Element of K6(REAL)
(f + a) | (['M0,Intf'] /\ ['M0,Intf']) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_in-infty (s + F) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V11() real ext-real set
left_closed_halfline a is V55() V56() V57() Element of K6(REAL)
K142(-infty,a) is set
(f,a) is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
Intf (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((Intf (#) f),a) is V11() real ext-real Element of REAL
Intf * (f,a) is V11() real ext-real Element of REAL
F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom F is V55() V56() V57() Element of K6(REAL)
lim_in-infty F is V11() real ext-real Element of REAL
Intf (#) F is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (Intf (#) F) is V55() V56() V57() Element of K6(REAL)
s is V11() real ext-real Element of REAL
(Intf (#) F) . s is V11() real ext-real Element of REAL
integral ((Intf (#) f),s,a) is V11() real ext-real Element of REAL
['s,a'] is non empty V55() V56() V57() V63() Element of K6(REAL)
[.s,a.] is V55() V56() V57() Element of K6(REAL)
f | ['s,a'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
F . s is V11() real ext-real Element of REAL
Intf * (F . s) is V11() real ext-real Element of REAL
integral (f,s,a) is V11() real ext-real Element of REAL
Intf * (integral (f,s,a)) is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
['s,a'] is non empty V55() V56() V57() V63() Element of K6(REAL)
(Intf (#) f) | ['s,a'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
[.s,a.] is V55() V56() V57() Element of K6(REAL)
f | ['s,a'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
lim_in-infty (Intf (#) F) is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
Intf (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
F is V11() real ext-real Element of REAL
F (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((F (#) f),a) is V11() real ext-real Element of REAL
F * (f,a) is V11() real ext-real Element of REAL
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
Intf is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
['a,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['a,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(f,a,Intf) is V11() real ext-real Element of REAL
integral (f,a,Intf) is V11() real ext-real Element of REAL
[.a,Intf.[ is V55() V56() V57() Element of K6(REAL)
F is non empty V55() V56() V57() Element of K6(REAL)
K7(F,REAL) is V41() V42() V43() set
K6(K7(F,REAL)) is set
s is V13() V16(F) V17( REAL ) V18() V27(F, REAL ) V41() V42() V43() Element of K6(K7(F,REAL))
dom s is V55() V56() V57() Element of K6(F)
K6(F) is set
['a,Intf'] /\ (dom f) is V55() V56() V57() Element of K6(REAL)
M0 is V11() real ext-real set
1 is non empty ordinal natural V11() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V66() V79() Element of NAT
M0 + 1 is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
f . r is V11() real ext-real Element of REAL
abs (f . r) is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( a <= b₁ & b₁ <= Intf ) } is set
[.a,Intf.] is V55() V56() V57() Element of K6(REAL)
f . a is V11() real ext-real Element of REAL
abs (f . a) is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
Intf - g is V11() real ext-real Element of REAL
- g is V11() real ext-real set
Intf + (- g) is V11() real ext-real set
(Intf - g) * M is V11() real ext-real Element of REAL
c₁₁ is V11() real ext-real Element of REAL
s . c₁₁ is V11() real ext-real Element of REAL
integral (f,a,c₁₁) is V11() real ext-real Element of REAL
Intf - c₁₁ is V11() real ext-real Element of REAL
- c₁₁ is V11() real ext-real set
Intf + (- c₁₁) is V11() real ext-real set
M * (Intf - g) is V11() real ext-real Element of REAL
M * (Intf - c₁₁) is V11() real ext-real Element of REAL
[.c₁₁,Intf.] is V55() V56() V57() Element of K6(REAL)
['c₁₁,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
c₁₂ is V11() real ext-real set
f . c₁₂ is V11() real ext-real Element of REAL
abs (f . c₁₂) is V11() real ext-real Element of REAL
integral (f,c₁₁,Intf) is V11() real ext-real Element of REAL
abs (integral (f,c₁₁,Intf)) is V11() real ext-real Element of REAL
(s . c₁₁) - (integral (f,a,Intf)) is V11() real ext-real Element of REAL
- (integral (f,a,Intf)) is V11() real ext-real set
(s . c₁₁) + (- (integral (f,a,Intf))) is V11() real ext-real set
abs ((s . c₁₁) - (integral (f,a,Intf))) is V11() real ext-real Element of REAL
(integral (f,a,Intf)) - (s . c₁₁) is V11() real ext-real Element of REAL
- (s . c₁₁) is V11() real ext-real set
(integral (f,a,Intf)) + (- (s . c₁₁)) is V11() real ext-real set
abs ((integral (f,a,Intf)) - (s . c₁₁)) is V11() real ext-real Element of REAL
(integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf)) is V11() real ext-real Element of REAL
((integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf))) - (integral (f,a,c₁₁)) is V11() real ext-real Element of REAL
- (integral (f,a,c₁₁)) is V11() real ext-real set
((integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf))) + (- (integral (f,a,c₁₁))) is V11() real ext-real set
abs (((integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf))) - (integral (f,a,c₁₁))) is V11() real ext-real Element of REAL
c₁₁ is V11() real ext-real Element of REAL
s . c₁₁ is V11() real ext-real Element of REAL
(s . c₁₁) - (integral (f,a,Intf)) is V11() real ext-real Element of REAL
(s . c₁₁) + (- (integral (f,a,Intf))) is V11() real ext-real set
abs ((s . c₁₁) - (integral (f,a,Intf))) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
s . r is V11() real ext-real Element of REAL
integral (f,a,r) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
a - a is V11() real ext-real Element of REAL
- a is V11() real ext-real set
a + (- a) is V11() real ext-real set
r - a is V11() real ext-real Element of REAL
r + (- a) is V11() real ext-real set
Intf - r is V11() real ext-real Element of REAL
- r is V11() real ext-real set
Intf + (- r) is V11() real ext-real set
(Intf - r) / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
(Intf - r) * (2 ") is V11() real ext-real set
r + ((Intf - r) / 2) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
(Intf - r) + r is V11() real ext-real Element of REAL
((Intf - r) / 2) + r is V11() real ext-real Element of REAL
g - 0 is V11() real ext-real Element of REAL
- 0 is empty V11() real ext-real non positive non negative V55() V56() V57() V58() V59() V60() V61() set
g + (- 0) is V11() real ext-real set
r - (r - a) is V11() real ext-real Element of REAL
- (r - a) is V11() real ext-real set
r + (- (r - a)) is V11() real ext-real set
lim_left (s,Intf) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
['a,r'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['a,r'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
Intf is V11() real ext-real Element of REAL
a is V11() real ext-real Element of REAL
['a,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['a,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(f,a,Intf) is V11() real ext-real Element of REAL
integral (f,a,Intf) is V11() real ext-real Element of REAL
].a,Intf.] is V55() V56() V57() Element of K6(REAL)
F is non empty V55() V56() V57() Element of K6(REAL)
K7(F,REAL) is V41() V42() V43() set
K6(K7(F,REAL)) is set
s is V13() V16(F) V17( REAL ) V18() V27(F, REAL ) V41() V42() V43() Element of K6(K7(F,REAL))
dom s is V55() V56() V57() Element of K6(F)
K6(F) is set
['a,Intf'] /\ (dom f) is V55() V56() V57() Element of K6(REAL)
M0 is V11() real ext-real set
1 is non empty ordinal natural V11() real ext-real positive non negative V55() V56() V57() V58() V59() V60() V66() V79() Element of NAT
M0 + 1 is V11() real ext-real Element of REAL
M is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
f . r is V11() real ext-real Element of REAL
abs (f . r) is V11() real ext-real Element of REAL
{ b₁ where b₁ is V11() real ext-real Element of REAL : ( a <= b₁ & b₁ <= Intf ) } is set
[.a,Intf.] is V55() V56() V57() Element of K6(REAL)
f . a is V11() real ext-real Element of REAL
abs (f . a) is V11() real ext-real Element of REAL
s is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom s is V55() V56() V57() Element of K6(REAL)
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
g - a is V11() real ext-real Element of REAL
- a is V11() real ext-real set
g + (- a) is V11() real ext-real set
(g - a) * M is V11() real ext-real Element of REAL
c₁₁ is V11() real ext-real Element of REAL
s . c₁₁ is V11() real ext-real Element of REAL
integral (f,c₁₁,Intf) is V11() real ext-real Element of REAL
c₁₁ - a is V11() real ext-real Element of REAL
c₁₁ + (- a) is V11() real ext-real set
M * (g - a) is V11() real ext-real Element of REAL
M * (c₁₁ - a) is V11() real ext-real Element of REAL
[.a,c₁₁.] is V55() V56() V57() Element of K6(REAL)
['a,c₁₁'] is non empty V55() V56() V57() V63() Element of K6(REAL)
c₁₂ is V11() real ext-real set
f . c₁₂ is V11() real ext-real Element of REAL
abs (f . c₁₂) is V11() real ext-real Element of REAL
integral (f,a,c₁₁) is V11() real ext-real Element of REAL
abs (integral (f,a,c₁₁)) is V11() real ext-real Element of REAL
(s . c₁₁) - (integral (f,a,Intf)) is V11() real ext-real Element of REAL
- (integral (f,a,Intf)) is V11() real ext-real set
(s . c₁₁) + (- (integral (f,a,Intf))) is V11() real ext-real set
abs ((s . c₁₁) - (integral (f,a,Intf))) is V11() real ext-real Element of REAL
(integral (f,a,Intf)) - (s . c₁₁) is V11() real ext-real Element of REAL
- (s . c₁₁) is V11() real ext-real set
(integral (f,a,Intf)) + (- (s . c₁₁)) is V11() real ext-real set
abs ((integral (f,a,Intf)) - (s . c₁₁)) is V11() real ext-real Element of REAL
(integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf)) is V11() real ext-real Element of REAL
((integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf))) - (integral (f,c₁₁,Intf)) is V11() real ext-real Element of REAL
- (integral (f,c₁₁,Intf)) is V11() real ext-real set
((integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf))) + (- (integral (f,c₁₁,Intf))) is V11() real ext-real set
abs (((integral (f,a,c₁₁)) + (integral (f,c₁₁,Intf))) - (integral (f,c₁₁,Intf))) is V11() real ext-real Element of REAL
c₁₁ is V11() real ext-real Element of REAL
s . c₁₁ is V11() real ext-real Element of REAL
(s . c₁₁) - (integral (f,a,Intf)) is V11() real ext-real Element of REAL
(s . c₁₁) + (- (integral (f,a,Intf))) is V11() real ext-real set
abs ((s . c₁₁) - (integral (f,a,Intf))) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
s . r is V11() real ext-real Element of REAL
integral (f,r,Intf) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
r - a is V11() real ext-real Element of REAL
- a is V11() real ext-real set
r + (- a) is V11() real ext-real set
(r - a) / 2 is V11() real ext-real Element of REAL
2 " is non empty V11() real ext-real positive non negative set
(r - a) * (2 ") is V11() real ext-real set
a + ((r - a) / 2) is V11() real ext-real Element of REAL
g is V11() real ext-real Element of REAL
(r - a) + a is V11() real ext-real Element of REAL
((r - a) / 2) + a is V11() real ext-real Element of REAL
lim_right (s,a) is V11() real ext-real Element of REAL
r is V11() real ext-real Element of REAL
['r,Intf'] is non empty V55() V56() V57() V63() Element of K6(REAL)
f | ['r,Intf'] is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
f is V11() real ext-real set
a is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
Intf is V11() real ext-real Element of REAL
a . Intf is V11() real ext-real Element of REAL
f * Intf is V11() real ext-real Element of REAL
- (f * Intf) is V11() real ext-real Element of REAL
exp_R . (- (f * Intf)) is V11() real ext-real Element of REAL
a is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
Intf is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
F is V11() real ext-real Element of REAL
a . F is V11() real ext-real Element of REAL
Intf . F is V11() real ext-real Element of REAL
f * F is V11() real ext-real Element of REAL
- (f * F) is V11() real ext-real Element of REAL
exp_R . (- (f * F)) is V11() real ext-real Element of REAL
right_open_halfline 0 is V55() V56() V57() Element of K6(REAL)
K143(0,+infty) is set
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
Intf is V11() real ext-real set
F is V11() real ext-real Element of REAL
(F) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
f (#) (F) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (F)),0) is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
a . Intf is V11() real ext-real Element of REAL
(Intf) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
f (#) (Intf) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (Intf)),0) is V11() real ext-real Element of REAL
a /. Intf is V11() real ext-real Element of REAL
Intf is V11() real ext-real Element of REAL
a . Intf is V11() real ext-real Element of REAL
(Intf) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
f (#) (Intf) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (Intf)),0) is V11() real ext-real Element of REAL
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
Intf is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom Intf is V55() V56() V57() Element of K6(REAL)
F is V11() real ext-real Element of REAL
a . F is V11() real ext-real Element of REAL
Intf . F is V11() real ext-real Element of REAL
(F) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
f (#) (F) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (F)),0) is V11() real ext-real Element of REAL
right_closed_halfline 0 is V55() V56() V57() Element of K6(REAL)
K141(0,+infty) is set
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom a is V55() V56() V57() Element of K6(REAL)
f + a is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f + a)) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(f) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(a) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(f) + (a) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom ((f) + (a)) is V55() V56() V57() Element of K6(REAL)
dom (f) is V55() V56() V57() Element of K6(REAL)
dom (a) is V55() V56() V57() Element of K6(REAL)
(dom (f)) /\ (dom (a)) is V55() V56() V57() Element of K6(REAL)
(right_open_halfline 0) /\ (dom (a)) is V55() V56() V57() Element of K6(REAL)
(right_open_halfline 0) /\ (right_open_halfline 0) is V55() V56() V57() Element of K6(REAL)
s is V11() real ext-real Element of REAL
(s) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
(f + a) (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(((f + a) (#) (s)),0) is V11() real ext-real Element of REAL
f (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (s)),0) is V11() real ext-real Element of REAL
a (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((a (#) (s)),0) is V11() real ext-real Element of REAL
((f (#) (s)),0) + ((a (#) (s)),0) is V11() real ext-real Element of REAL
(f (#) (s)) + (a (#) (s)) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (a (#) (s)) is V55() V56() V57() Element of K6(REAL)
dom (s) is V55() V56() V57() Element of K6(REAL)
(dom a) /\ (dom (s)) is V55() V56() V57() Element of K6(REAL)
(right_closed_halfline 0) /\ REAL is V55() V56() V57() Element of K6(REAL)
dom (f (#) (s)) is V55() V56() V57() Element of K6(REAL)
(dom f) /\ (dom (s)) is V55() V56() V57() Element of K6(REAL)
s is V11() real ext-real Element of REAL
((f) + (a)) . s is V11() real ext-real Element of REAL
(s) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
(f + a) (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(((f + a) (#) (s)),0) is V11() real ext-real Element of REAL
f (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (s)),0) is V11() real ext-real Element of REAL
a (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((a (#) (s)),0) is V11() real ext-real Element of REAL
((f (#) (s)),0) + ((a (#) (s)),0) is V11() real ext-real Element of REAL
(f) . s is V11() real ext-real Element of REAL
((f) . s) + ((a (#) (s)),0) is V11() real ext-real Element of REAL
(a) . s is V11() real ext-real Element of REAL
((f) . s) + ((a) . s) is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
(s) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
(f + a) (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom f is V55() V56() V57() Element of K6(REAL)
(f) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a is V11() real ext-real Element of REAL
a (#) f is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((a (#) f)) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
a (#) (f) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (a (#) (f)) is V55() V56() V57() Element of K6(REAL)
dom (f) is V55() V56() V57() Element of K6(REAL)
s is V11() real ext-real Element of REAL
(s) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
(a (#) f) (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(((a (#) f) (#) (s)),0) is V11() real ext-real Element of REAL
f (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (s)),0) is V11() real ext-real Element of REAL
a * ((f (#) (s)),0) is V11() real ext-real Element of REAL
a (#) (f (#) (s)) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
dom (f (#) (s)) is V55() V56() V57() Element of K6(REAL)
dom (s) is V55() V56() V57() Element of K6(REAL)
(dom f) /\ (dom (s)) is V55() V56() V57() Element of K6(REAL)
(right_closed_halfline 0) /\ REAL is V55() V56() V57() Element of K6(REAL)
s is V11() real ext-real Element of REAL
(a (#) (f)) . s is V11() real ext-real Element of REAL
(s) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
(a (#) f) (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
(((a (#) f) (#) (s)),0) is V11() real ext-real Element of REAL
f (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))
((f (#) (s)),0) is V11() real ext-real Element of REAL
a * ((f (#) (s)),0) is V11() real ext-real Element of REAL
(f) . s is V11() real ext-real Element of REAL
a * ((f) . s) is V11() real ext-real Element of REAL
s is V11() real ext-real Element of REAL
(s) is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V41() V42() V43() Element of K6(K7(REAL,REAL))
(a (#) f) (#) (s) is V13() V16( REAL ) V17( REAL ) V18() V41() V42() V43() Element of K6(K7(REAL,REAL))