:: INTEGRA1 semantic presentation

REAL is non empty non trivial V40() V64() V65() V66() V70() V85() non bounded_below non bounded_above interval set

bool REAL is non empty non trivial V40() set

bool omega is non empty non trivial V40() set
bool NAT is non empty non trivial V40() set
K147(NAT) is V39() set
{} is set
RAT is non empty non trivial V40() V64() V65() V66() V67() V70() set

{{},1} is V40() set
COMPLEX is non empty non trivial V40() V64() V70() set
INT is non empty non trivial V40() V64() V65() V66() V67() V68() V70() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set

bool is non empty non trivial V40() set
K347() is set
ExtREAL is non empty V65() interval set

bool is non empty non trivial V40() set

{1} is non empty trivial V40() V44() 1 -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded set
Seg 2 is non empty V40() 2 -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
{1,2} is V40() V44() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded set
A is V64() V65() V66() Element of bool REAL
f is V22() real ext-real set
g is V22() real ext-real set
[.f,g.] is V64() V65() V66() interval Element of bool REAL
A is non empty compact V64() V65() V66() interval closed_interval Element of bool REAL
A is V64() V65() V66() Element of bool REAL

[.(),().] is V64() V65() V66() interval Element of bool REAL
f is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.f,g.] is V64() V65() V66() interval Element of bool REAL
a1 is V22() real ext-real set
g - a1 is V22() real ext-real Element of REAL
g + a1 is V22() real ext-real Element of REAL
(g + a1) - a1 is V22() real ext-real Element of REAL
a1 is V22() real ext-real set
{ b1 where b1 is V22() real ext-real Element of REAL : ( f <= b1 & b1 <= g ) } is set
D1 is V22() real ext-real Element of REAL
a1 is V22() real ext-real set
{ b1 where b1 is V22() real ext-real Element of REAL : ( f <= b1 & b1 <= g ) } is set
D1 is V22() real ext-real Element of REAL
a1 is V22() real ext-real set
f + a1 is V22() real ext-real Element of REAL

f is V22() real ext-real set
a1 is V22() real ext-real set
[.f,a1.] is V64() V65() V66() interval Element of bool REAL
g is V22() real ext-real set
D1 is V22() real ext-real set
[.g,D1.] is V64() V65() V66() interval Element of bool REAL
A is non empty compact V64() V65() V66() Element of bool REAL

bool [:(Seg 1),REAL:] is non empty non trivial V40() set

bool is non empty non trivial V40() set

dom g is non empty trivial V40() 1 -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool (Seg 1)
bool (Seg 1) is non empty V40() V44() set

dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

a1 . D1 is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real Element of REAL

a1 . (len a1) is V22() real ext-real Element of REAL
A is non empty compact V64() V65() V66() Element of bool REAL

bool is non empty non trivial V40() set
f is set
g is set

f is set
g is set
a1 is set
A is non empty compact V64() V65() V66() Element of bool REAL
(A) is set

A is non empty compact V64() V65() V66() Element of bool REAL
(A) is non empty set
f is Element of (A)
g is Element of (A)
A is non empty compact V64() V65() V66() Element of bool REAL
(A) is non empty set
f is Relation-like Function-like Element of (A)
g is Relation-like Function-like Element of (A)

dom g is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
g . A is V22() real ext-real Element of REAL

A - 1 is V22() real ext-real Element of REAL

dom g is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
g . (A - 1) is V22() real ext-real Element of REAL

Seg a1 is V40() a1 -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

(1 + 1) - 1 is V22() real ext-real Element of REAL
a1 - 0 is V22() real ext-real Element of REAL

2 - 1 is V22() real ext-real Element of REAL
A - (2 - 1) is V22() real ext-real Element of REAL

dom f is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

f . g is V22() real ext-real Element of REAL
g - 1 is V22() real ext-real Element of REAL
f . (g - 1) is V22() real ext-real Element of REAL
[.(),(f . g).] is V64() V65() V66() interval Element of bool REAL
a1 is V64() V65() V66() Element of bool REAL

[.(),().] is V64() V65() V66() interval Element of bool REAL
- 1 is V22() real ext-real non positive Element of REAL
1 + (- 1) is V22() real ext-real Element of REAL
g + (1 + (- 1)) is V22() real ext-real Element of REAL
g + (- 1) is V22() real ext-real Element of REAL
D1 is V22() real ext-real Element of REAL
D1 is V22() real ext-real Element of REAL
[.D1,D1.] is V64() V65() V66() interval Element of bool REAL
a2 is V64() V65() V66() Element of bool REAL

f . a1 is V22() real ext-real Element of REAL

[.(),().] is V64() V65() V66() interval Element of bool REAL

inf a1 is V22() real ext-real set

sup a1 is V22() real ext-real set

inf D1 is V22() real ext-real set

sup D1 is V22() real ext-real set
D1 is V22() real ext-real Element of REAL
[.(),D1.] is V64() V65() V66() interval Element of bool REAL
D1 is V22() real ext-real Element of REAL
a2 is V22() real ext-real Element of REAL
[.D1,a2.] is V64() V65() V66() interval Element of bool REAL

dom g is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

[.(),().] is V64() V65() V66() interval Element of bool REAL
lower_bound (f,g,A) is V22() real ext-real Element of REAL
inf (f,g,A) is V22() real ext-real set
g . A is V22() real ext-real Element of REAL
a1 is V22() real ext-real Element of REAL
upper_bound (f,g,A) is V22() real ext-real Element of REAL
sup (f,g,A) is V22() real ext-real set
[.(),a1.] is V64() V65() V66() interval Element of bool REAL
g . A is V22() real ext-real Element of REAL

[.(),().] is V64() V65() V66() interval Element of bool REAL
A - 1 is V22() real ext-real Element of REAL
g . (A - 1) is V22() real ext-real Element of REAL
[.(g . (A - 1)),(g . A).] is V64() V65() V66() interval Element of bool REAL
upper_bound (f,g,A) is V22() real ext-real Element of REAL
sup (f,g,A) is V22() real ext-real set
lower_bound (f,g,A) is V22() real ext-real Element of REAL
inf (f,g,A) is V22() real ext-real set
A is V64() V65() V66() Element of bool REAL

() - () is V22() real ext-real Element of REAL
A is non empty V64() V65() V66() bounded_below bounded_above real-bounded Element of bool REAL
(A) is V22() real ext-real Element of REAL

() - () is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set

dom g is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

a1 . D1 is V22() real ext-real Element of REAL
(A,g,D1) is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL

rng (f | (A,g,D1)) is V64() V65() V66() Element of bool REAL
upper_bound (rng (f | (A,g,D1))) is V22() real ext-real Element of REAL
((A,g,D1)) is V22() real ext-real Element of REAL
upper_bound (A,g,D1) is V22() real ext-real Element of REAL
sup (A,g,D1) is V22() real ext-real set
lower_bound (A,g,D1) is V22() real ext-real Element of REAL
inf (A,g,D1) is V22() real ext-real set
(upper_bound (A,g,D1)) - (lower_bound (A,g,D1)) is V22() real ext-real Element of REAL
(upper_bound (rng (f | (A,g,D1)))) * ((A,g,D1)) is V22() real ext-real Element of REAL

dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

a1 . D1 is V22() real ext-real Element of REAL
D1 . D1 is V22() real ext-real Element of REAL
(A,g,D1) is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL

rng (f | (A,g,D1)) is V64() V65() V66() Element of bool REAL
upper_bound (rng (f | (A,g,D1))) is V22() real ext-real Element of REAL
((A,g,D1)) is V22() real ext-real Element of REAL
upper_bound (A,g,D1) is V22() real ext-real Element of REAL
sup (A,g,D1) is V22() real ext-real set
lower_bound (A,g,D1) is V22() real ext-real Element of REAL
inf (A,g,D1) is V22() real ext-real set
(upper_bound (A,g,D1)) - (lower_bound (A,g,D1)) is V22() real ext-real Element of REAL
(upper_bound (rng (f | (A,g,D1)))) * ((A,g,D1)) is V22() real ext-real Element of REAL

dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

a1 . D1 is V22() real ext-real Element of REAL
(A,g,D1) is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL

rng (f | (A,g,D1)) is V64() V65() V66() Element of bool REAL
lower_bound (rng (f | (A,g,D1))) is V22() real ext-real Element of REAL
((A,g,D1)) is V22() real ext-real Element of REAL
upper_bound (A,g,D1) is V22() real ext-real Element of REAL
sup (A,g,D1) is V22() real ext-real set
lower_bound (A,g,D1) is V22() real ext-real Element of REAL
inf (A,g,D1) is V22() real ext-real set
(upper_bound (A,g,D1)) - (lower_bound (A,g,D1)) is V22() real ext-real Element of REAL
(lower_bound (rng (f | (A,g,D1)))) * ((A,g,D1)) is V22() real ext-real Element of REAL

dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

a1 . D1 is V22() real ext-real Element of REAL
D1 . D1 is V22() real ext-real Element of REAL
(A,g,D1) is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL

rng (f | (A,g,D1)) is V64() V65() V66() Element of bool REAL
lower_bound (rng (f | (A,g,D1))) is V22() real ext-real Element of REAL
((A,g,D1)) is V22() real ext-real Element of REAL
upper_bound (A,g,D1) is V22() real ext-real Element of REAL
sup (A,g,D1) is V22() real ext-real set
lower_bound (A,g,D1) is V22() real ext-real Element of REAL
inf (A,g,D1) is V22() real ext-real set
(upper_bound (A,g,D1)) - (lower_bound (A,g,D1)) is V22() real ext-real Element of REAL
(lower_bound (rng (f | (A,g,D1)))) * ((A,g,D1)) is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set

Sum (A,f,g) is V22() real ext-real Element of REAL

K173(REAL,(A,f,g),K295()) is V22() real ext-real Element of REAL

Sum (A,f,g) is V22() real ext-real Element of REAL
K173(REAL,(A,f,g),K295()) is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set
(A) is non empty set

bool [:(A),REAL:] is non empty non trivial V40() set

(A,f,D1) is V22() real ext-real Element of REAL

Sum (A,f,D1) is V22() real ext-real Element of REAL
K173(REAL,(A,f,D1),K295()) is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real Element of REAL
(A,f,D1) is V22() real ext-real Element of REAL

Sum (A,f,D1) is V22() real ext-real Element of REAL
K173(REAL,(A,f,D1),K295()) is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real Element of REAL

(A,f,a2) is V22() real ext-real Element of REAL

Sum (A,f,a2) is V22() real ext-real Element of REAL
K173(REAL,(A,f,a2),K295()) is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real set
D1 . D1 is V22() real ext-real set
a1 . D1 is V22() real ext-real Element of REAL

(A,f,a2) is V22() real ext-real Element of REAL

Sum (A,f,a2) is V22() real ext-real Element of REAL
K173(REAL,(A,f,a2),K295()) is V22() real ext-real Element of REAL
D1 . D1 is V22() real ext-real Element of REAL

(A,f,D1) is V22() real ext-real Element of REAL

Sum (A,f,D1) is V22() real ext-real Element of REAL
K173(REAL,(A,f,D1),K295()) is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real Element of REAL
(A,f,D1) is V22() real ext-real Element of REAL

Sum (A,f,D1) is V22() real ext-real Element of REAL
K173(REAL,(A,f,D1),K295()) is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real Element of REAL

(A,f,a2) is V22() real ext-real Element of REAL

Sum (A,f,a2) is V22() real ext-real Element of REAL
K173(REAL,(A,f,a2),K295()) is V22() real ext-real Element of REAL

a1 . D1 is V22() real ext-real set
D1 . D1 is V22() real ext-real set
a1 . D1 is V22() real ext-real Element of REAL

(A,f,a2) is V22() real ext-real Element of REAL

Sum (A,f,a2) is V22() real ext-real Element of REAL
K173(REAL,(A,f,a2),K295()) is V22() real ext-real Element of REAL
D1 . D1 is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set

bool [:A,REAL:] is non empty non trivial V40() set

(A) is non empty set

bool [:(A),REAL:] is non empty non trivial V40() set
rng (A,f) is non empty V64() V65() V66() Element of bool REAL
lower_bound (rng (A,f)) is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set

(A) is non empty set

bool [:(A),REAL:] is non empty non trivial V40() set
rng (A,f) is non empty V64() V65() V66() Element of bool REAL
upper_bound (rng (A,f)) is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set

bool [:A,REAL:] is non empty non trivial V40() set

(A,f) is V22() real ext-real Element of REAL

(A) is non empty set

bool [:(A),REAL:] is non empty non trivial V40() set
rng (A,f) is non empty V64() V65() V66() Element of bool REAL
lower_bound (rng (A,f)) is V22() real ext-real Element of REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

rng (f + g) is V64() V65() V66() Element of bool REAL
rng f is V64() V65() V66() Element of bool REAL
rng g is V64() V65() V66() Element of bool REAL
(rng f) ++ (rng g) is V64() V65() V66() set
(rng f) ++ (rng g) is V65() set
a1 is set
dom (f + g) is Element of bool A
bool A is non empty set
D1 is set
(f + g) . D1 is V22() real ext-real Element of REAL
dom f is Element of bool A
dom g is Element of bool A
(dom f) /\ (dom g) is Element of bool A
f . D1 is V22() real ext-real Element of REAL
g . D1 is V22() real ext-real Element of REAL
(f . D1) + (g . D1) is V22() real ext-real Element of REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

rng f is V64() V65() V66() Element of bool REAL
dom f is Element of bool A
bool A is non empty set
A /\ (dom f) is Element of bool A
g is V22() real ext-real set
a1 is ext-real set
D1 is set
f . D1 is V22() real ext-real Element of REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

rng f is V64() V65() V66() Element of bool REAL

g is V22() real ext-real set
dom f is Element of bool A
bool A is non empty set
A /\ (dom f) is Element of bool A
a1 is set
f . a1 is V22() real ext-real Element of REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

rng f is V64() V65() V66() Element of bool REAL
dom f is Element of bool A
bool A is non empty set
A /\ (dom f) is Element of bool A
g is V22() real ext-real set
a1 is ext-real set
D1 is set
f . D1 is V22() real ext-real Element of REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

rng f is V64() V65() V66() Element of bool REAL

g is V22() real ext-real set
dom f is Element of bool A
bool A is non empty set
A /\ (dom f) is Element of bool A
a1 is set
f . a1 is V22() real ext-real Element of REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

rng f is V64() V65() V66() Element of bool REAL
A is non empty set

bool [:A,REAL:] is non empty non trivial V40() set

dom (chi (A,A)) is Element of bool A
bool A is non empty set
A /\ (dom (chi (A,A))) is Element of bool A
f is Element of A
(chi (A,A)) /. f is V22() real ext-real Element of REAL
(chi (A,A)) . f is V22() real ext-real Element of REAL
{1} is non empty trivial V40() V44() 1 -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
A is non empty set
bool A is non empty set
f is non empty Element of bool A

bool [:f,REAL:] is non empty non trivial V40() set
rng (chi (f,f)) is V64() V65() V66() Element of bool REAL

dom (chi (f,f)) is Element of bool f
bool f is non empty set
f /\ (dom (chi (f,f))) is Element of bool f
g is Element of A
(chi (f,f)) . g is V22() real ext-real Element of REAL
g is Element of A
(chi (f,f)) . g is V22() real ext-real Element of REAL
rng ((chi (f,f)) | f) is V64() V65() V66() Element of bool REAL
g is V22() real ext-real Element of REAL

A is non empty set
bool A is non empty set
f is non empty Element of bool A

bool [:f,REAL:] is non empty non trivial V40() set
dom (chi (f,f)) is Element of bool f
bool f is non empty set
g is set

rng ((chi (f,f)) | g) is V64() V65() V66() Element of bool REAL
dom ((chi (f,f)) | g) is Element of bool f
g /\ (dom (chi (f,f))) is Element of bool f
rng (chi (f,f)) is V64() V65() V66() Element of bool REAL

bool [:f,REAL:] is non empty non trivial V40() set

dom g is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

((f,g,A)) is V22() real ext-real Element of REAL
upper_bound (f,g,A) is V22() real ext-real Element of REAL
sup (f,g,A) is V22() real ext-real set
lower_bound (f,g,A) is V22() real ext-real Element of REAL
inf (f,g,A) is V22() real ext-real set
(upper_bound (f,g,A)) - (lower_bound (f,g,A)) is V22() real ext-real Element of REAL

(f,(chi (f,f)),g) . A is V22() real ext-real Element of REAL
dom (chi (f,f)) is V64() V65() V66() Element of bool f
bool f is non empty set
(chi (f,f)) | (f,g,A) is Relation-like f -defined (f,g,A) -defined f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng ((chi (f,f)) | (f,g,A)) is V64() V65() V66() Element of bool REAL
lower_bound (rng ((chi (f,f)) | (f,g,A))) is V22() real ext-real Element of REAL
(lower_bound (rng ((chi (f,f)) | (f,g,A)))) * ((f,g,A)) is V22() real ext-real Element of REAL
(f,g,A) /\ (dom (chi (f,f))) is V64() V65() V66() Element of bool f
rng (chi (f,f)) is V64() V65() V66() Element of bool REAL
lower_bound (rng (chi (f,f))) is V22() real ext-real Element of REAL

bool [:f,REAL:] is non empty non trivial V40() set

dom g is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

((f,g,A)) is V22() real ext-real Element of REAL
upper_bound (f,g,A) is V22() real ext-real Element of REAL
sup (f,g,A) is V22() real ext-real set
lower_bound (f,g,A) is V22() real ext-real Element of REAL
inf (f,g,A) is V22() real ext-real set
(upper_bound (f,g,A)) - (lower_bound (f,g,A)) is V22() real ext-real Element of REAL

(f,(chi (f,f)),g) . A is V22() real ext-real Element of REAL
dom (chi (f,f)) is V64() V65() V66() Element of bool f
bool f is non empty set
(chi (f,f)) | (f,g,A) is Relation-like f -defined (f,g,A) -defined f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
rng ((chi (f,f)) | (f,g,A)) is V64() V65() V66() Element of bool REAL
upper_bound (rng ((chi (f,f)) | (f,g,A))) is V22() real ext-real Element of REAL
(upper_bound (rng ((chi (f,f)) | (f,g,A)))) * ((f,g,A)) is V22() real ext-real Element of REAL
(f,g,A) /\ (dom (chi (f,f))) is V64() V65() V66() Element of bool f
rng (chi (f,f)) is V64() V65() V66() Element of bool REAL
upper_bound (rng (chi (f,f))) is V22() real ext-real Element of REAL

dom A is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

K173(REAL,A,K295()) is V22() real ext-real Element of REAL

K173(REAL,f,K295()) is V22() real ext-real Element of REAL
(Sum A) + (Sum f) is V22() real ext-real Element of REAL

K173(REAL,g,K295()) is V22() real ext-real Element of REAL

K178(K295(),A,f) is set

dom g is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len (A + f)) is V40() len (A + f) -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

g . a1 is V22() real ext-real Element of REAL
A . a1 is V22() real ext-real Element of REAL
f . a1 is V22() real ext-real Element of REAL
(A . a1) + (f . a1) is V22() real ext-real Element of REAL
Seg (len f) is V40() len f -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
dom f is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
f /. a1 is V22() real ext-real Element of REAL
A /. a1 is V22() real ext-real Element of REAL

g . a1 is V22() real ext-real Element of REAL
(A + f) . a1 is V22() real ext-real Element of REAL
A . a1 is V22() real ext-real Element of REAL
f . a1 is V22() real ext-real Element of REAL
(A . a1) + (f . a1) is V22() real ext-real Element of REAL
dom (A + f) is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Sum (A + f) is V22() real ext-real Element of REAL
K173(REAL,(A + f),K295()) is V22() real ext-real Element of REAL

dom A is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

K173(REAL,A,K295()) is V22() real ext-real Element of REAL

K173(REAL,f,K295()) is V22() real ext-real Element of REAL
(Sum A) - (Sum f) is V22() real ext-real Element of REAL

K173(REAL,g,K295()) is V22() real ext-real Element of REAL

K178(K296(),A,f) is set

dom g is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len (A - f)) is V40() len (A - f) -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

g . a1 is V22() real ext-real Element of REAL
A . a1 is V22() real ext-real Element of REAL
f . a1 is V22() real ext-real Element of REAL
(A . a1) - (f . a1) is V22() real ext-real Element of REAL
Seg (len f) is V40() len f -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
dom f is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
f /. a1 is V22() real ext-real Element of REAL
A /. a1 is V22() real ext-real Element of REAL

g . a1 is V22() real ext-real Element of REAL
(A - f) . a1 is V22() real ext-real Element of REAL
Seg (len A) is V40() len A -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
A . a1 is V22() real ext-real Element of REAL
f . a1 is V22() real ext-real Element of REAL
(A . a1) - (f . a1) is V22() real ext-real Element of REAL
dom (A - f) is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Sum (A - f) is V22() real ext-real Element of REAL
K173(REAL,(A - f),K295()) is V22() real ext-real Element of REAL

bool [:A,REAL:] is non empty non trivial V40() set
(A) is V22() real ext-real Element of REAL

() - () is V22() real ext-real Element of REAL

Sum (A,(chi (A,A)),f) is V22() real ext-real Element of REAL
K173(REAL,(A,(chi (A,A)),f),K295()) is V22() real ext-real Element of REAL

dom g is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Seg (len f) is non empty V40() len f -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

g . a1 is V22() real ext-real Element of REAL
(A,f,a1) is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
upper_bound (A,f,a1) is V22() real ext-real Element of REAL
sup (A,f,a1) is V22() real ext-real set
lower_bound (A,f,a1) is V22() real ext-real Element of REAL
inf (A,f,a1) is V22() real ext-real set
(upper_bound (A,f,a1)) - (lower_bound (A,f,a1)) is V22() real ext-real Element of REAL
((A,f,a1)) is V22() real ext-real Element of REAL
(len f) - 1 is V22() real ext-real Element of REAL

dom D1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

dom D1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Seg a1 is V40() a1 -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT

dom (D1 ^ <*()*>) is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

g . a2 is V22() real ext-real Element of REAL
(D1 ^ <*()*>) /. a2 is V22() real ext-real Element of REAL
(<*()*> ^ D1) /. a2 is V22() real ext-real Element of REAL
((D1 ^ <*()*>) /. a2) - ((<*()*> ^ D1) /. a2) is V22() real ext-real Element of REAL
(D1 ^ <*()*>) . a2 is V22() real ext-real Element of REAL
Seg (len (D1 ^ <*()*>)) is non empty V40() len (D1 ^ <*()*>) -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (<*()*> ^ D1) is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
(<*()*> ^ D1) . a2 is V22() real ext-real Element of REAL
dom f is non empty V40() V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
f . a2 is V22() real ext-real Element of REAL
(A,f,a2) is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
upper_bound (A,f,a2) is V22() real ext-real Element of REAL
sup (A,f,a2) is V22() real ext-real set
lower_bound (A,f,a2) is V22() real ext-real Element of REAL
inf (A,f,a2) is V22() real ext-real set
(upper_bound (A,f,a2)) - (lower_bound (A,f,a2)) is V22() real ext-real Element of REAL
2 - 1 is V22() real ext-real Element of REAL
<*()*> . a2 is V22() real ext-real Element of REAL
D1 . a2 is