:: INTEGRA1 semantic presentation

REAL is non empty non trivial V40() V64() V65() V66() V70() V85() non bounded_below non bounded_above interval set
NAT is non empty non trivial epsilon-transitive epsilon-connected ordinal V40() cardinal limit_cardinal V64() V65() V66() V67() V68() V69() V70() V85() left_end bounded_below Element of bool REAL
bool REAL is non empty non trivial V40() set
omega is non empty non trivial epsilon-transitive epsilon-connected ordinal V40() cardinal limit_cardinal V64() V65() V66() V67() V68() V69() V70() V85() left_end bounded_below 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
the Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V64() V65() V66() V67() V68() V69() V70() bounded_below bounded_above real-bounded interval set is Relation-like non-empty empty-yielding RAT -valued functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V40() V41() V44() cardinal {} -element FinSequence-like FinSequence-membered complex-valued ext-real-valued real-valued natural-valued V64() V65() V66() V67() V68() V69() V70() bounded_below bounded_above real-bounded interval set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
{{},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
[:COMPLEX,COMPLEX:] is Relation-like non empty non trivial V40() complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty non trivial V40() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is Relation-like non empty non trivial V40() complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty non trivial V40() set
[:REAL,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty non trivial V40() set
[:[:REAL,REAL:],REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty non trivial V40() set
[:RAT,RAT:] is Relation-like RAT -valued non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty non trivial V40() set
[:[:RAT,RAT:],RAT:] is Relation-like RAT -valued non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty non trivial V40() set
[:INT,INT:] is Relation-like RAT -valued INT -valued non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty non trivial V40() set
[:[:INT,INT:],INT:] is Relation-like RAT -valued INT -valued non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty non trivial V40() set
[:NAT,NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V40() complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is Relation-like RAT -valued INT -valued non empty non trivial V40() complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty non trivial V40() set
K347() is set
ExtREAL is non empty V65() interval set
[:COMPLEX,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is non empty non trivial V40() set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
Seg 1 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 NAT
{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
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
lower_bound A is V22() real ext-real Element of REAL
inf A is V22() real ext-real set
upper_bound A is V22() real ext-real Element of REAL
sup A is V22() real ext-real set
[.(lower_bound A),(upper_bound A).] 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
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f <= b₁ & b₁ <= g ) } is set
D1 is V22() real ext-real Element of REAL
a1 is V22() real ext-real set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f <= b₁ & b₁ <= 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
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool 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
upper_bound A is V22() real ext-real Element of REAL
[:(Seg 1),REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:(Seg 1),REAL:] is non empty non trivial V40() set
(Seg 1) --> (upper_bound A) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
[:NAT,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty non trivial V40() set
g is Relation-like Seg 1 -defined REAL -valued Function-like non empty total V30( Seg 1, REAL ) V40() complex-valued ext-real-valued real-valued Element of bool [:(Seg 1),REAL:]
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
rng g is non empty V40() V64() V65() V66() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
a1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
a1 . D1 is V22() real ext-real Element of REAL
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
a1 . D1 is V22() real ext-real Element of REAL
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
a1 . D1 is V22() real ext-real Element of REAL
rng a1 is V40() V64() V65() V66() bounded_below bounded_above real-bounded Element of bool REAL
len a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
a1 . (len a1) is V22() real ext-real Element of REAL
A is non empty compact V64() V65() V66() Element of bool REAL
[:NAT,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty non trivial V40() set
f is set
g is set
a1 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
f is set
g is set
a1 is set
A is non empty compact V64() V65() V66() Element of bool REAL
(A) is set
the Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A) is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
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)
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
f is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (f)
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
rng g is non empty V40() V64() V65() V66() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
A - 1 is V22() real ext-real Element of REAL
f is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (f)
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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
Seg a1 is V40() a1 -element V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
2 + D1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
(1 + 1) - 1 is V22() real ext-real Element of REAL
a1 - 0 is V22() real ext-real Element of REAL
rng g is non empty V40() V64() V65() V66() left_end right_end bounded_below bounded_above real-bounded Element of bool REAL
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
D1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
2 - 1 is V22() real ext-real Element of REAL
A - (2 - 1) is V22() real ext-real Element of REAL
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
g is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
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
lower_bound A is V22() real ext-real Element of REAL
inf A is V22() real ext-real set
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
[.(lower_bound A),(f . g).] is V64() V65() V66() interval Element of bool REAL
a1 is V64() V65() V66() Element of bool REAL
lower_bound a1 is V22() real ext-real Element of REAL
upper_bound a1 is V22() real ext-real Element of REAL
[.(lower_bound a1),(upper_bound a1).] 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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
f . a1 is V22() real ext-real Element of REAL
lower_bound a2 is V22() real ext-real Element of REAL
upper_bound a2 is V22() real ext-real Element of REAL
[.(lower_bound a2),(upper_bound a2).] is V64() V65() V66() interval Element of bool REAL
a1 is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
lower_bound a1 is V22() real ext-real Element of REAL
inf a1 is V22() real ext-real set
upper_bound a1 is V22() real ext-real Element of REAL
sup a1 is V22() real ext-real set
D1 is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
lower_bound D1 is V22() real ext-real Element of REAL
inf D1 is V22() real ext-real set
upper_bound D1 is V22() real ext-real Element of REAL
sup D1 is V22() real ext-real set
D1 is V22() real ext-real Element of REAL
[.(lower_bound A),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
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
f is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (f)
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 non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
lower_bound f is V22() real ext-real Element of REAL
inf f is V22() real ext-real set
upper_bound f is V22() real ext-real Element of REAL
sup f is V22() real ext-real set
[.(lower_bound f),(upper_bound f).] 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
[.(lower_bound f),a1.] is V64() V65() V66() interval Element of bool REAL
g . A is V22() real ext-real Element of REAL
lower_bound f is V22() real ext-real Element of REAL
inf f is V22() real ext-real set
upper_bound f is V22() real ext-real Element of REAL
sup f is V22() real ext-real set
[.(lower_bound f),(upper_bound f).] 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
upper_bound A is V22() real ext-real Element of REAL
lower_bound A is V22() real ext-real Element of REAL
(upper_bound A) - (lower_bound A) 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
upper_bound A is V22() real ext-real Element of REAL
sup A is V22() real ext-real set
lower_bound A is V22() real ext-real Element of REAL
inf A is V22() real ext-real set
(upper_bound A) - (lower_bound A) is V22() real ext-real Element of REAL
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
len g is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
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 is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
a1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
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
f | (A,g,D1) is Relation-like A -defined (A,g,D1) -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
a1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
D1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
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
f | (A,g,D1) is Relation-like A -defined (A,g,D1) -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
a1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
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
f | (A,g,D1) is Relation-like A -defined (A,g,D1) -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
a1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
D1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom a1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
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
f | (A,g,D1) is Relation-like A -defined (A,g,D1) -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,g) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
Sum (A,f,g) is V22() real ext-real Element of REAL
K295() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K173(REAL,(A,f,g),K295()) is V22() real ext-real Element of REAL
(A,f,g) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
(A) is non empty set
[:(A),REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:(A),REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
a1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (A)
D1 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,D1) is V22() real ext-real Element of REAL
(A,f,D1) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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 is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
D1 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
a1 . D1 is V22() real ext-real Element of REAL
(A,f,D1) is V22() real ext-real Element of REAL
(A,f,D1) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
D1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (A)
a1 . D1 is V22() real ext-real Element of REAL
a2 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,a2) is V22() real ext-real Element of REAL
(A,f,a2) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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 is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
D1 is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
D1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (A)
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
a2 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,a2) is V22() real ext-real Element of REAL
(A,f,a2) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
a1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (A)
D1 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,D1) is V22() real ext-real Element of REAL
(A,f,D1) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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 is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
D1 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
a1 . D1 is V22() real ext-real Element of REAL
(A,f,D1) is V22() real ext-real Element of REAL
(A,f,D1) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
D1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (A)
a1 . D1 is V22() real ext-real Element of REAL
a2 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,a2) is V22() real ext-real Element of REAL
(A,f,a2) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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 is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
D1 is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
D1 is Relation-like NAT -defined Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued Element of (A)
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
a2 is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,f,a2) is V22() real ext-real Element of REAL
(A,f,a2) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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 is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(A,f) is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
(A) is non empty set
[:(A),REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued 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 compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(A,f) is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
(A) is non empty set
[:(A),REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued 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
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
(A,f) is V22() real ext-real Element of REAL
(A,f) is Relation-like (A) -defined REAL -valued Function-like non empty total V30((A), REAL ) complex-valued ext-real-valued real-valued Element of bool [:(A),REAL:]
(A) is non empty set
[:(A),REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued 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
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
g is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
f + g is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
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
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
f | A is Relation-like A -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
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
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng f is V64() V65() V66() Element of bool REAL
f | A is Relation-like A -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
f | A is Relation-like A -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
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
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng f is V64() V65() V66() Element of bool REAL
f | A is Relation-like A -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,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
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
f is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
f | A is Relation-like A -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
rng f is V64() V65() V66() Element of bool REAL
A is non empty set
chi (A,A) is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
(chi (A,A)) | A is Relation-like A -defined A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
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
chi (f,f) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non empty non trivial V40() set
rng (chi (f,f)) is V64() V65() V66() Element of bool REAL
(chi (f,f)) | f is Relation-like f -defined f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,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
{g} is non empty trivial V40() 1 -element V64() V65() V66() 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
chi (f,f) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
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
(chi (f,f)) | g is Relation-like f -defined g -defined f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
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
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
f is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
chi (f,f) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non empty non trivial V40() set
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (f)
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 non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
((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) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
f is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
chi (f,f) is Relation-like f -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:f,REAL:]
[:f,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:f,REAL:] is non empty non trivial V40() set
g is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (f)
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 non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
((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) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
A is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom A is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Sum A is V22() real ext-real Element of REAL
K173(REAL,A,K295()) is V22() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
Sum f 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
g is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len g is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
Sum g is V22() real ext-real Element of REAL
K173(REAL,g,K295()) is V22() real ext-real Element of REAL
(len A) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
A + f is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K178(K295(),A,f) is set
len (A + f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of 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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
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
A is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len A is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom A is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
Sum A is V22() real ext-real Element of REAL
K173(REAL,A,K295()) is V22() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len f is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
Sum f 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
g is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len g is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
Sum g is V22() real ext-real Element of REAL
K173(REAL,g,K295()) is V22() real ext-real Element of REAL
(len A) -tuples_on REAL is functional non empty FinSequence-membered FinSequenceSet of REAL
A - f is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
K296() is Relation-like [:REAL,REAL:] -defined REAL -valued Function-like non empty total V30([:REAL,REAL:], REAL ) complex-valued ext-real-valued real-valued Element of bool [:[:REAL,REAL:],REAL:]
K178(K296(),A,f) is set
len (A - f) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of 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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
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
A is non empty compact V64() V65() V66() bounded_below bounded_above real-bounded interval closed_interval Element of bool REAL
chi (A,A) is Relation-like A -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:A,REAL:]
[:A,REAL:] is Relation-like non empty non trivial V40() complex-valued ext-real-valued real-valued set
bool [:A,REAL:] is non empty non trivial V40() set
(A) is V22() real ext-real Element of REAL
upper_bound A is V22() real ext-real Element of REAL
sup A is V22() real ext-real set
lower_bound A is V22() real ext-real Element of REAL
inf A is V22() real ext-real set
(upper_bound A) - (lower_bound A) is V22() real ext-real Element of REAL
f is Relation-like NAT -defined REAL -valued Function-like one-to-one non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing non-decreasing (A)
(A,(chi (A,A)),f) is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence 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
len f is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
g is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len g is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of 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
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal set
1 + a1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
a1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
D1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
dom D1 is V40() V64() V65() V66() V67() V68() V69() bounded_below bounded_above real-bounded Element of bool NAT
D1 is Relation-like NAT -defined REAL -valued Function-like V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len D1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of 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
<*(upper_bound A)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
D1 ^ <*(upper_bound A)*> is Relation-like NAT -defined REAL -valued Function-like non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (D1 ^ <*(upper_bound A)*>) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
<*(lower_bound A)*> is Relation-like NAT -defined REAL -valued Function-like one-to-one constant non empty trivial V40() 1 -element FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued increasing decreasing non-decreasing non-increasing FinSequence of REAL
<*(lower_bound A)*> ^ D1 is Relation-like NAT -defined REAL -valued Function-like non empty V40() FinSequence-like FinSubsequence-like complex-valued ext-real-valued real-valued FinSequence of REAL
len (<*(lower_bound A)*> ^ D1) is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom (D1 ^ <*(upper_bound A)*>) 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 <*(upper_bound A)*> 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 NAT
len <*(upper_bound A)*> is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
a1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
dom <*(lower_bound A)*> 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 NAT
len <*(lower_bound A)*> is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() left_end right_end bounded_below bounded_above real-bounded Element of NAT
a2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V40() cardinal V64() V65() V66() V67() V68() V69() V71() V72() bounded_below bounded_above real-bounded Element of NAT
g . a2 is V22() real ext-real Element of REAL
(D1 ^ <*(upper_bound A)*>) /. a2 is V22() real ext-real Element of REAL
(<*(lower_bound A)*> ^ D1) /. a2 is V22() real ext-real Element of REAL
((D1 ^ <*(upper_bound A)*>) /. a2) - ((<*(lower_bound A)*> ^ D1) /. a2) is V22() real ext-real Element of REAL
(D1 ^ <*(upper_bound A)*>) . a2 is V22() real ext-real Element of REAL
Seg (len (D1 ^ <*(upper_bound A)*>)) is non empty V40() len (D1 ^ <*(upper_bound A)*>) -element V64() V65() V66() V67() V68() V69() left_end right_end bounded_below bounded_above real-bounded Element of bool NAT
dom (<*(lower_bound A)*> ^ 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
(<*(lower_bound A)*> ^ 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
<*(lower_bound A)*> . a2 is V22() real ext-real Element of REAL
D1 . a2 is