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

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

a1 is V22() real ext-real set

{ b

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