:: FCONT_2 semantic presentation

REAL is non empty V45() V46() V47() V51() V52() non bounded_below non bounded_above V69() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() left_end bounded_below Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V45() V51() V52() set
RAT is non empty V45() V46() V47() V48() V51() V52() set
INT is non empty V45() V46() V47() V48() V49() V51() V52() set
omega is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() left_end bounded_below set
K19(omega) is set
K19(NAT) is set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V45() V46() V47() V48() V49() V50() V51() bounded_below V69() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
{{},1} is non empty V45() V46() V47() V48() V49() V50() left_end bounded_below set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is V5( RAT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is V5( RAT ) V5( INT ) complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() Element of NAT
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
{0} is non empty V45() V46() V47() V48() V49() V50() left_end bounded_below set
{0} is non empty V45() V46() V47() V48() V49() V50() left_end bounded_below Element of K19(REAL)
2 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
K19(K20(NAT,NAT)) is set
p is set
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (g | p) is V45() V46() V47() Element of K19(REAL)
f is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
g . x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
x2 - s is V22() real ext-real Element of REAL
abs (x2 - s) is V22() real ext-real Element of REAL
g . s is V22() real ext-real Element of REAL
(g . x2) - (g . s) is V22() real ext-real Element of REAL
abs ((g . x2) - (g . s)) is V22() real ext-real Element of REAL
(g | p) . s is V22() real ext-real Element of REAL
(g | p) . x2 is V22() real ext-real Element of REAL
f is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
(g | p) . x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
x2 - s is V22() real ext-real Element of REAL
abs (x2 - s) is V22() real ext-real Element of REAL
(g | p) . s is V22() real ext-real Element of REAL
((g | p) . x2) - ((g | p) . s) is V22() real ext-real Element of REAL
abs (((g | p) . x2) - ((g | p) . s)) is V22() real ext-real Element of REAL
g . s is V22() real ext-real Element of REAL
g . x2 is V22() real ext-real Element of REAL
p is set
g is set
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f | g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
y is V22() real ext-real Element of REAL
dom (f | p) is V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
dom (f | g) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
x1 - x1 is V22() real ext-real Element of REAL
abs (x1 - x1) is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(f . x1) - (f . x1) is V22() real ext-real Element of REAL
abs ((f . x1) - (f . x1)) is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom y is V45() V46() V47() Element of K19(REAL)
y | g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f + y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f + y) | (p /\ g) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(dom f) /\ (dom y) is V45() V46() V47() Element of K19(REAL)
dom (f + y) is V45() V46() V47() Element of K19(REAL)
y | (p /\ g) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f | (p /\ g) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V22() real ext-real Element of REAL
x2 / 2 is V22() real ext-real Element of REAL
dom (f | (p /\ g)) is V45() V46() V47() Element of K19(REAL)
s is V22() real ext-real Element of REAL
dom (y | (p /\ g)) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
min (s,x1) is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
dom ((f + y) | (p /\ g)) is V45() V46() V47() Element of K19(REAL)
r is V22() real ext-real Element of REAL
x2 - r is V22() real ext-real Element of REAL
abs (x2 - r) is V22() real ext-real Element of REAL
y . x2 is V22() real ext-real Element of REAL
y . r is V22() real ext-real Element of REAL
(y . x2) - (y . r) is V22() real ext-real Element of REAL
abs ((y . x2) - (y . r)) is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
f . r is V22() real ext-real Element of REAL
(f . x2) - (f . r) is V22() real ext-real Element of REAL
abs ((f . x2) - (f . r)) is V22() real ext-real Element of REAL
(x2 / 2) + (x2 / 2) is V22() real ext-real Element of REAL
(abs ((f . x2) - (f . r))) + (abs ((y . x2) - (y . r))) is V22() real ext-real Element of REAL
((f . x2) - (f . r)) + ((y . x2) - (y . r)) is V22() real ext-real Element of REAL
abs (((f . x2) - (f . r)) + ((y . x2) - (y . r))) is V22() real ext-real Element of REAL
(f + y) . x2 is V22() real ext-real Element of REAL
(f + y) . r is V22() real ext-real Element of REAL
((f + y) . x2) - ((f + y) . r) is V22() real ext-real Element of REAL
abs (((f + y) . x2) - ((f + y) . r)) is V22() real ext-real Element of REAL
(f . x2) + (y . x2) is V22() real ext-real Element of REAL
((f . x2) + (y . x2)) - ((f + y) . r) is V22() real ext-real Element of REAL
abs (((f . x2) + (y . x2)) - ((f + y) . r)) is V22() real ext-real Element of REAL
(f . r) + (y . r) is V22() real ext-real Element of REAL
((f . x2) + (y . x2)) - ((f . r) + (y . r)) is V22() real ext-real Element of REAL
abs (((f . x2) + (y . x2)) - ((f . r) + (y . r))) is V22() real ext-real Element of REAL
p is set
g is set
p /\ g is set
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom y is V45() V46() V47() Element of K19(REAL)
y | g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f - y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- y is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) y is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
f + (- y) is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
(f - y) | (p /\ g) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(dom f) /\ (dom y) is V45() V46() V47() Element of K19(REAL)
dom (f - y) is V45() V46() V47() Element of K19(REAL)
y | (p /\ g) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f | (p /\ g) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V22() real ext-real Element of REAL
x2 / 2 is V22() real ext-real Element of REAL
dom (f | (p /\ g)) is V45() V46() V47() Element of K19(REAL)
s is V22() real ext-real Element of REAL
dom (y | (p /\ g)) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
min (s,x1) is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
dom ((f - y) | (p /\ g)) is V45() V46() V47() Element of K19(REAL)
r is V22() real ext-real Element of REAL
x2 - r is V22() real ext-real Element of REAL
abs (x2 - r) is V22() real ext-real Element of REAL
y . x2 is V22() real ext-real Element of REAL
y . r is V22() real ext-real Element of REAL
(y . x2) - (y . r) is V22() real ext-real Element of REAL
abs ((y . x2) - (y . r)) is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
f . r is V22() real ext-real Element of REAL
(f . x2) - (f . r) is V22() real ext-real Element of REAL
abs ((f . x2) - (f . r)) is V22() real ext-real Element of REAL
(x2 / 2) + (x2 / 2) is V22() real ext-real Element of REAL
(abs ((f . x2) - (f . r))) + (abs ((y . x2) - (y . r))) is V22() real ext-real Element of REAL
((f . x2) - (f . r)) - ((y . x2) - (y . r)) is V22() real ext-real Element of REAL
abs (((f . x2) - (f . r)) - ((y . x2) - (y . r))) is V22() real ext-real Element of REAL
(f - y) . x2 is V22() real ext-real Element of REAL
(f - y) . r is V22() real ext-real Element of REAL
((f - y) . x2) - ((f - y) . r) is V22() real ext-real Element of REAL
abs (((f - y) . x2) - ((f - y) . r)) is V22() real ext-real Element of REAL
(f . x2) - (y . x2) is V22() real ext-real Element of REAL
((f . x2) - (y . x2)) - ((f - y) . r) is V22() real ext-real Element of REAL
abs (((f . x2) - (y . x2)) - ((f - y) . r)) is V22() real ext-real Element of REAL
(f . r) - (y . r) is V22() real ext-real Element of REAL
((f . x2) - (y . x2)) - ((f . r) - (y . r)) is V22() real ext-real Element of REAL
abs (((f . x2) - (y . x2)) - ((f . r) - (y . r))) is V22() real ext-real Element of REAL
p is set
g is V22() real ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
g (#) f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(g (#) f) | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (g (#) f) is V45() V46() V47() Element of K19(REAL)
y is V22() real ext-real Element of REAL
dom (f | p) is V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
dom ((g (#) f) | p) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
x1 - x1 is V22() real ext-real Element of REAL
abs (x1 - x1) is V22() real ext-real Element of REAL
(g (#) f) . x1 is V22() real ext-real Element of REAL
(g (#) f) . x1 is V22() real ext-real Element of REAL
((g (#) f) . x1) - ((g (#) f) . x1) is V22() real ext-real Element of REAL
abs (((g (#) f) . x1) - ((g (#) f) . x1)) is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
g * (f . x1) is V22() real ext-real Element of REAL
(g * (f . x1)) - ((g (#) f) . x1) is V22() real ext-real Element of REAL
abs ((g * (f . x1)) - ((g (#) f) . x1)) is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
g * (f . x1) is V22() real ext-real Element of REAL
0 - (g * (f . x1)) is V22() real ext-real Element of REAL
abs (0 - (g * (f . x1))) is V22() real ext-real Element of REAL
abs g is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
y / (abs g) is V22() real ext-real Element of REAL
dom (f | p) is V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
dom ((g (#) f) | p) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
x1 - x1 is V22() real ext-real Element of REAL
abs (x1 - x1) is V22() real ext-real Element of REAL
(g (#) f) . x1 is V22() real ext-real Element of REAL
(g (#) f) . x1 is V22() real ext-real Element of REAL
((g (#) f) . x1) - ((g (#) f) . x1) is V22() real ext-real Element of REAL
abs (((g (#) f) . x1) - ((g (#) f) . x1)) is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
g * (f . x1) is V22() real ext-real Element of REAL
(g * (f . x1)) - ((g (#) f) . x1) is V22() real ext-real Element of REAL
abs ((g * (f . x1)) - ((g (#) f) . x1)) is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
g * (f . x1) is V22() real ext-real Element of REAL
(g * (f . x1)) - (g * (f . x1)) is V22() real ext-real Element of REAL
abs ((g * (f . x1)) - (g * (f . x1))) is V22() real ext-real Element of REAL
(f . x1) - (f . x1) is V22() real ext-real Element of REAL
g * ((f . x1) - (f . x1)) is V22() real ext-real Element of REAL
abs (g * ((f . x1) - (f . x1))) is V22() real ext-real Element of REAL
abs ((f . x1) - (f . x1)) is V22() real ext-real Element of REAL
(abs g) * (abs ((f . x1) - (f . x1))) is V22() real ext-real Element of REAL
(y / (abs g)) * (abs g) is V22() real ext-real Element of REAL
p is set
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom g is V45() V46() V47() Element of K19(REAL)
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- 1 is V22() real ext-real non positive set
(- 1) (#) g is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
(- g) | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- 1 is V22() real ext-real non positive Element of REAL
(- 1) (#) g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is set
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
abs g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(abs g) | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f is V22() real ext-real Element of REAL
dom (g | p) is V45() V46() V47() Element of K19(REAL)
y is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
dom ((abs g) | p) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
s - x1 is V22() real ext-real Element of REAL
abs (s - x1) is V22() real ext-real Element of REAL
dom (abs g) is V45() V46() V47() Element of K19(REAL)
dom g is V45() V46() V47() Element of K19(REAL)
(abs g) . s is V22() real ext-real Element of REAL
(abs g) . x1 is V22() real ext-real Element of REAL
((abs g) . s) - ((abs g) . x1) is V22() real ext-real Element of REAL
abs (((abs g) . s) - ((abs g) . x1)) is V22() real ext-real Element of REAL
g . s is V22() real ext-real Element of REAL
abs (g . s) is V22() real ext-real Element of REAL
(abs (g . s)) - ((abs g) . x1) is V22() real ext-real Element of REAL
abs ((abs (g . s)) - ((abs g) . x1)) is V22() real ext-real Element of REAL
g . x1 is V22() real ext-real Element of REAL
abs (g . x1) is V22() real ext-real Element of REAL
(abs (g . s)) - (abs (g . x1)) is V22() real ext-real Element of REAL
abs ((abs (g . s)) - (abs (g . x1))) is V22() real ext-real Element of REAL
(g . s) - (g . x1) is V22() real ext-real Element of REAL
abs ((g . s) - (g . x1)) is V22() real ext-real Element of REAL
p is set
g is set
f is set
p /\ f is set
(p /\ f) /\ g is set
y is set
((p /\ f) /\ g) /\ y is set
x2 is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom x2 is V45() V46() V47() Element of K19(REAL)
x2 | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 | f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V45() V46() V47() Element of K19(REAL)
s | g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s | y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 (#) s is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(x2 (#) s) | (((p /\ f) /\ g) /\ y) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f /\ (dom x2) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real set
y /\ (dom s) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real set
x2 is V22() real ext-real Element of REAL
abs x2 is V22() real ext-real Element of REAL
(abs x2) + 1 is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
abs r is V22() real ext-real Element of REAL
(abs r) + 1 is V22() real ext-real Element of REAL
max (((abs x2) + 1),((abs r) + 1)) is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
g /\ y is set
(p /\ f) /\ (g /\ y) is set
x2 . r is V22() real ext-real Element of REAL
abs (x2 . r) is V22() real ext-real Element of REAL
x2 + 0 is V22() real ext-real Element of REAL
s . r is V22() real ext-real Element of REAL
abs (s . r) is V22() real ext-real Element of REAL
r + 0 is V22() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() Element of NAT
2 * (max (((abs x2) + 1),((abs r) + 1))) is V22() real ext-real Element of REAL
dom ((x2 (#) s) | (((p /\ f) /\ g) /\ y)) is V45() V46() V47() Element of K19(REAL)
r is V22() real ext-real Element of REAL
r / (2 * (max (((abs x2) + 1),((abs r) + 1)))) is V22() real ext-real Element of REAL
dom (x2 | p) is V45() V46() V47() Element of K19(REAL)
s is V22() real ext-real Element of REAL
dom (s | g) is V45() V46() V47() Element of K19(REAL)
g is V22() real ext-real Element of REAL
min (s,g) is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
y1 is V22() real ext-real Element of REAL
y2 is V22() real ext-real Element of REAL
y1 - y2 is V22() real ext-real Element of REAL
abs (y1 - y2) is V22() real ext-real Element of REAL
(x2 (#) s) . y1 is V22() real ext-real Element of REAL
(x2 (#) s) . y2 is V22() real ext-real Element of REAL
((x2 (#) s) . y1) - ((x2 (#) s) . y2) is V22() real ext-real Element of REAL
abs (((x2 (#) s) . y1) - ((x2 (#) s) . y2)) is V22() real ext-real Element of REAL
s . y1 is V22() real ext-real Element of REAL
s . y2 is V22() real ext-real Element of REAL
(s . y1) - (s . y2) is V22() real ext-real Element of REAL
abs ((s . y1) - (s . y2)) is V22() real ext-real Element of REAL
x2 . y1 is V22() real ext-real Element of REAL
(x2 . y1) * (s . y1) is V22() real ext-real Element of REAL
((x2 . y1) * (s . y1)) - ((x2 (#) s) . y2) is V22() real ext-real Element of REAL
abs (((x2 . y1) * (s . y1)) - ((x2 (#) s) . y2)) is V22() real ext-real Element of REAL
(x2 . y1) * (s . y2) is V22() real ext-real Element of REAL
((x2 . y1) * (s . y2)) - ((x2 . y1) * (s . y2)) is V22() real ext-real Element of REAL
((x2 . y1) * (s . y1)) + (((x2 . y1) * (s . y2)) - ((x2 . y1) * (s . y2))) is V22() real ext-real Element of REAL
x2 . y2 is V22() real ext-real Element of REAL
(x2 . y2) * (s . y2) is V22() real ext-real Element of REAL
(((x2 . y1) * (s . y1)) + (((x2 . y1) * (s . y2)) - ((x2 . y1) * (s . y2)))) - ((x2 . y2) * (s . y2)) is V22() real ext-real Element of REAL
abs ((((x2 . y1) * (s . y1)) + (((x2 . y1) * (s . y2)) - ((x2 . y1) * (s . y2)))) - ((x2 . y2) * (s . y2))) is V22() real ext-real Element of REAL
(x2 . y1) * ((s . y1) - (s . y2)) is V22() real ext-real Element of REAL
(x2 . y1) - (x2 . y2) is V22() real ext-real Element of REAL
((x2 . y1) - (x2 . y2)) * (s . y2) is V22() real ext-real Element of REAL
((x2 . y1) * ((s . y1) - (s . y2))) + (((x2 . y1) - (x2 . y2)) * (s . y2)) is V22() real ext-real Element of REAL
abs (((x2 . y1) * ((s . y1) - (s . y2))) + (((x2 . y1) - (x2 . y2)) * (s . y2))) is V22() real ext-real Element of REAL
abs ((x2 . y1) * ((s . y1) - (s . y2))) is V22() real ext-real Element of REAL
abs (((x2 . y1) - (x2 . y2)) * (s . y2)) is V22() real ext-real Element of REAL
(abs ((x2 . y1) * ((s . y1) - (s . y2)))) + (abs (((x2 . y1) - (x2 . y2)) * (s . y2))) is V22() real ext-real Element of REAL
abs (x2 . y1) is V22() real ext-real Element of REAL
(abs (x2 . y1)) * (abs ((s . y1) - (s . y2))) is V22() real ext-real Element of REAL
abs (s . y2) is V22() real ext-real Element of REAL
abs ((x2 . y1) - (x2 . y2)) is V22() real ext-real Element of REAL
(abs (s . y2)) * (abs ((x2 . y1) - (x2 . y2))) is V22() real ext-real Element of REAL
(max (((abs x2) + 1),((abs r) + 1))) * (r / (2 * (max (((abs x2) + 1),((abs r) + 1))))) is V22() real ext-real Element of REAL
((max (((abs x2) + 1),((abs r) + 1))) * (r / (2 * (max (((abs x2) + 1),((abs r) + 1)))))) + ((max (((abs x2) + 1),((abs r) + 1))) * (r / (2 * (max (((abs x2) + 1),((abs r) + 1)))))) is V22() real ext-real Element of REAL
(max (((abs x2) + 1),((abs r) + 1))) * 2 is V22() real ext-real Element of REAL
r / ((max (((abs x2) + 1),((abs r) + 1))) * 2) is V22() real ext-real Element of REAL
(r / ((max (((abs x2) + 1),((abs r) + 1))) * 2)) + (r / ((max (((abs x2) + 1),((abs r) + 1))) * 2)) is V22() real ext-real Element of REAL
(max (((abs x2) + 1),((abs r) + 1))) * ((r / ((max (((abs x2) + 1),((abs r) + 1))) * 2)) + (r / ((max (((abs x2) + 1),((abs r) + 1))) * 2))) is V22() real ext-real Element of REAL
r / (max (((abs x2) + 1),((abs r) + 1))) is V22() real ext-real Element of REAL
(r / (max (((abs x2) + 1),((abs r) + 1)))) * (max (((abs x2) + 1),((abs r) + 1))) is V22() real ext-real Element of REAL
p is set
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom g is V45() V46() V47() Element of K19(REAL)
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f is V22() real ext-real set
y is V22() real ext-real set
dom (g | p) is V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
s is V22() real ext-real set
x1 is V22() real ext-real set
x1 is V22() real ext-real set
x1 - f is V22() real ext-real set
abs (x1 - f) is V22() real ext-real Element of REAL
g . x1 is V22() real ext-real Element of REAL
g . f is V22() real ext-real Element of REAL
(g . x1) - (g . f) is V22() real ext-real Element of REAL
abs ((g . x1) - (g . f)) is V22() real ext-real Element of REAL
p is set
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (g | p) is V45() V46() V47() Element of K19(REAL)
f is V22() real ext-real set
x2 is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
x2 / y is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
x1 - x1 is V22() real ext-real Element of REAL
abs (x1 - x1) is V22() real ext-real Element of REAL
s * y is V22() real ext-real Element of REAL
y * (abs (x1 - x1)) is V22() real ext-real Element of REAL
g . x1 is V22() real ext-real Element of REAL
g . x1 is V22() real ext-real Element of REAL
(g . x1) - (g . x1) is V22() real ext-real Element of REAL
abs ((g . x1) - (g . x1)) is V22() real ext-real Element of REAL
(x2 / y) * y is V22() real ext-real Element of REAL
p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom p is V45() V46() V47() Element of K19(REAL)
g is V45() V46() V47() Element of K19(REAL)
p | g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (p | g) is V45() V46() V47() Element of K19(REAL)
f is V22() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
1 / (y + 1) is V22() real ext-real non negative Element of REAL
x2 is V22() real ext-real Element of REAL
p . x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
p . s is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
x2 - x1 is V22() real ext-real Element of REAL
abs (x2 - x1) is V22() real ext-real Element of REAL
p . x1 is V22() real ext-real Element of REAL
(p . x2) - (p . x1) is V22() real ext-real Element of REAL
abs ((p . x2) - (p . x1)) is V22() real ext-real Element of REAL
y is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x2 is set
rng y is V45() V46() V47() Element of K19(REAL)
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
y . s is V22() real ext-real Element of REAL
x2 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim x2 is V22() real ext-real Element of REAL
rng x2 is V45() V46() V47() Element of K19(REAL)
(dom p) /\ g is V45() V46() V47() Element of K19(REAL)
(p | g) . (lim x2) is V22() real ext-real Element of REAL
(p | g) /* x2 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
lim ((p | g) /* x2) is V22() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
1 / (s + 1) is V22() real ext-real non negative Element of REAL
y . s is V22() real ext-real Element of REAL
p . (y . s) is V22() real ext-real Element of REAL
s is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x1 is set
rng s is V45() V46() V47() Element of K19(REAL)
x1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
s . x1 is V22() real ext-real Element of REAL
x1 is V1() V4( NAT ) V5( NAT ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))
y * x1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
y - s is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- s is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) s is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
y + (- s) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(y - s) * x1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
x2 - ((y - s) * x1) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- ((y - s) * x1) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((y - s) * x1) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
x2 + (- ((y - s) * x1)) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
x2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
(x2 - ((y - s) * x1)) . x2 is V22() real ext-real Element of REAL
(y * x1) . x2 is V22() real ext-real Element of REAL
((y - s) * x1) . x2 is V22() real ext-real Element of REAL
((y * x1) . x2) - (((y - s) * x1) . x2) is V22() real ext-real Element of REAL
x1 . x2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
y . (x1 . x2) is V22() real ext-real Element of REAL
(y . (x1 . x2)) - (((y - s) * x1) . x2) is V22() real ext-real Element of REAL
(y - s) . (x1 . x2) is V22() real ext-real Element of REAL
(y . (x1 . x2)) - ((y - s) . (x1 . x2)) is V22() real ext-real Element of REAL
s . (x1 . x2) is V22() real ext-real Element of REAL
(y . (x1 . x2)) - (s . (x1 . x2)) is V22() real ext-real Element of REAL
(y . (x1 . x2)) - ((y . (x1 . x2)) - (s . (x1 . x2))) is V22() real ext-real Element of REAL
s * x1 is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(s * x1) . x2 is V22() real ext-real Element of REAL
rng (x2 - ((y - s) * x1)) is V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real set
x2 " is V22() real ext-real set
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
1 / (s + 1) is V22() real ext-real non negative Element of REAL
1 / (s + 1) is V22() real ext-real non negative Element of REAL
y . s is V22() real ext-real Element of REAL
s . s is V22() real ext-real Element of REAL
(y . s) - (s . s) is V22() real ext-real Element of REAL
abs ((y . s) - (s . s)) is V22() real ext-real Element of REAL
1 / (x2 ") is V22() real ext-real Element of REAL
(y - s) . s is V22() real ext-real Element of REAL
((y - s) . s) - 0 is V22() real ext-real Element of REAL
abs (((y - s) . s) - 0) is V22() real ext-real Element of REAL
lim (y - s) is V22() real ext-real Element of REAL
lim ((y - s) * x1) is V22() real ext-real Element of REAL
lim (x2 - ((y - s) * x1)) is V22() real ext-real Element of REAL
(lim x2) - 0 is V22() real ext-real Element of REAL
(p | g) /* (x2 - ((y - s) * x1)) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
((p | g) /* x2) - ((p | g) /* (x2 - ((y - s) * x1))) is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- ((p | g) /* (x2 - ((y - s) * x1))) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) ((p | g) /* (x2 - ((y - s) * x1))) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
((p | g) /* x2) + (- ((p | g) /* (x2 - ((y - s) * x1)))) is V1() V4( NAT ) Function-like total complex-valued ext-real-valued real-valued set
lim ((p | g) /* (x2 - ((y - s) * x1))) is V22() real ext-real Element of REAL
lim (((p | g) /* x2) - ((p | g) /* (x2 - ((y - s) * x1)))) is V22() real ext-real Element of REAL
((p | g) . (lim x2)) - ((p | g) . (lim x2)) is V22() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
x2 . r is V22() real ext-real Element of REAL
(x2 - ((y - s) * x1)) . r is V22() real ext-real Element of REAL
(((p | g) /* x2) - ((p | g) /* (x2 - ((y - s) * x1)))) . r is V22() real ext-real Element of REAL
((((p | g) /* x2) - ((p | g) /* (x2 - ((y - s) * x1)))) . r) - 0 is V22() real ext-real Element of REAL
abs (((((p | g) /* x2) - ((p | g) /* (x2 - ((y - s) * x1)))) . r) - 0) is V22() real ext-real Element of REAL
((p | g) /* x2) . r is V22() real ext-real Element of REAL
((p | g) /* (x2 - ((y - s) * x1))) . r is V22() real ext-real Element of REAL
(((p | g) /* x2) . r) - (((p | g) /* (x2 - ((y - s) * x1))) . r) is V22() real ext-real Element of REAL
abs ((((p | g) /* x2) . r) - (((p | g) /* (x2 - ((y - s) * x1))) . r)) is V22() real ext-real Element of REAL
(p | g) . (x2 . r) is V22() real ext-real Element of REAL
((p | g) . (x2 . r)) - (((p | g) /* (x2 - ((y - s) * x1))) . r) is V22() real ext-real Element of REAL
abs (((p | g) . (x2 . r)) - (((p | g) /* (x2 - ((y - s) * x1))) . r)) is V22() real ext-real Element of REAL
(p | g) . ((x2 - ((y - s) * x1)) . r) is V22() real ext-real Element of REAL
((p | g) . (x2 . r)) - ((p | g) . ((x2 - ((y - s) * x1)) . r)) is V22() real ext-real Element of REAL
abs (((p | g) . (x2 . r)) - ((p | g) . ((x2 - ((y - s) * x1)) . r))) is V22() real ext-real Element of REAL
p . (x2 . r) is V22() real ext-real Element of REAL
(p . (x2 . r)) - ((p | g) . ((x2 - ((y - s) * x1)) . r)) is V22() real ext-real Element of REAL
abs ((p . (x2 . r)) - ((p | g) . ((x2 - ((y - s) * x1)) . r))) is V22() real ext-real Element of REAL
p . ((x2 - ((y - s) * x1)) . r) is V22() real ext-real Element of REAL
(p . (x2 . r)) - (p . ((x2 - ((y - s) * x1)) . r)) is V22() real ext-real Element of REAL
abs ((p . (x2 . r)) - (p . ((x2 - ((y - s) * x1)) . r))) is V22() real ext-real Element of REAL
x1 . r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
y . (x1 . r) is V22() real ext-real Element of REAL
p . (y . (x1 . r)) is V22() real ext-real Element of REAL
(s * x1) . r is V22() real ext-real Element of REAL
p . ((s * x1) . r) is V22() real ext-real Element of REAL
(p . (y . (x1 . r))) - (p . ((s * x1) . r)) is V22() real ext-real Element of REAL
abs ((p . (y . (x1 . r))) - (p . ((s * x1) . r))) is V22() real ext-real Element of REAL
s . (x1 . r) is V22() real ext-real Element of REAL
p . (s . (x1 . r)) is V22() real ext-real Element of REAL
(p . (y . (x1 . r))) - (p . (s . (x1 . r))) is V22() real ext-real Element of REAL
abs ((p . (y . (x1 . r))) - (p . (s . (x1 . r)))) is V22() real ext-real Element of REAL
p is V45() V46() V47() Element of K19(REAL)
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom g is V45() V46() V47() Element of K19(REAL)
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
g .: p is V45() V46() V47() Element of K19(REAL)
p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom p is V45() V46() V47() Element of K19(REAL)
g is V45() V46() V47() Element of K19(REAL)
p | g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p .: g is V45() V46() V47() Element of K19(REAL)
upper_bound (p .: g) is V22() real ext-real Element of REAL
lower_bound (p .: g) is V22() real ext-real Element of REAL
f is V22() real ext-real set
y is V22() real ext-real set
p . f is V22() real ext-real Element of REAL
p . y is V22() real ext-real Element of REAL
p is set
g is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom g is V45() V46() V47() Element of K19(REAL)
g | p is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V45() V46() V47() V69() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f . p is V22() real ext-real Element of REAL
f . g is V22() real ext-real Element of REAL
[.(f . p),(f . g).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . g),(f . p).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . p),(f . g).] \/ [.(f . g),(f . p).] is V45() V46() V47() Element of K19(REAL)
y is V22() real ext-real Element of REAL
K20([.p,g.],REAL) is complex-valued ext-real-valued real-valued set
K19(K20([.p,g.],REAL)) is set
[.p,g.] --> y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
[.(f . p),(f . g).] \/ {} is V45() V46() V47() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . p <= b₁ & b₁ <= f . g ) } is set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
x2 is V1() V4([.p,g.]) V5( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20([.p,g.],REAL))
s is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V45() V46() V47() Element of K19(REAL)
(dom s) /\ (dom f) is V45() V46() V47() Element of K19(REAL)
s - f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) f is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
s + (- f) is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
dom (s - f) is V45() V46() V47() Element of K19(REAL)
abs (s - f) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(abs (s - f)) " {0} is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
dom (abs (s - f)) is V45() V46() V47() Element of K19(REAL)
(abs (s - f)) . x1 is V22() real ext-real Element of REAL
(s - f) . x1 is V22() real ext-real Element of REAL
abs ((s - f) . x1) is V22() real ext-real Element of REAL
s . x1 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(s . x1) - (f . x1) is V22() real ext-real Element of REAL
y - (f . x1) is V22() real ext-real Element of REAL
(abs (s - f)) ^ is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((abs (s - f)) ^) is V45() V46() V47() Element of K19(REAL)
dom (abs (s - f)) is V45() V46() V47() Element of K19(REAL)
(dom (abs (s - f))) \ ((abs (s - f)) " {0}) is V45() V46() V47() Element of K19(REAL)
[.p,g.] /\ (dom f) is V45() V46() V47() Element of K19(REAL)
[.p,g.] /\ (dom s) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
s . x1 is V22() real ext-real Element of REAL
s | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(s - f) | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(abs (s - f)) | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs (s - f)) ^) | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs (s - f)) ^) .: [.p,g.] is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real set
x1 is V22() real ext-real set
abs x1 is V22() real ext-real Element of REAL
(abs x1) + 1 is V22() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() Element of NAT
((abs x1) + 1) " is V22() real ext-real Element of REAL
1 / ((abs x1) + 1) is V22() real ext-real Element of REAL
dom (f | [.p,g.]) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
((abs (s - f)) ^) . x2 is V22() real ext-real Element of REAL
(abs (s - f)) . x2 is V22() real ext-real Element of REAL
((abs (s - f)) . x2) " is V22() real ext-real Element of REAL
(s - f) . x2 is V22() real ext-real Element of REAL
abs ((s - f) . x2) is V22() real ext-real Element of REAL
(abs ((s - f) . x2)) " is V22() real ext-real Element of REAL
s . x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
(s . x2) - (f . x2) is V22() real ext-real Element of REAL
abs ((s . x2) - (f . x2)) is V22() real ext-real Element of REAL
(abs ((s . x2) - (f . x2))) " is V22() real ext-real Element of REAL
y - (f . x2) is V22() real ext-real Element of REAL
abs (y - (f . x2)) is V22() real ext-real Element of REAL
(abs (y - (f . x2))) " is V22() real ext-real Element of REAL
x1 + 0 is V22() real ext-real Element of REAL
1 / ((abs (y - (f . x2))) ") is V22() real ext-real Element of REAL
g - p is V22() real ext-real Element of REAL
(g - p) / x1 is V22() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
x1 * x2 is V22() real ext-real Element of REAL
((g - p) / x1) * x1 is V22() real ext-real Element of REAL
(x1 * x2) / x2 is V22() real ext-real Element of REAL
(g - p) / x2 is V22() real ext-real Element of REAL
x2 " is V22() real ext-real non negative Element of REAL
(x1 * x2) * (x2 ") is V22() real ext-real Element of REAL
x2 * (x2 ") is V22() real ext-real non negative Element of REAL
x1 * (x2 * (x2 ")) is V22() real ext-real Element of REAL
x1 * 1 is V22() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
((g - p) / x2) * x2 is V22() real ext-real Element of REAL
((g - p) / x2) * s is V22() real ext-real Element of REAL
p + (g - p) is V22() real ext-real Element of REAL
p + (((g - p) / x2) * s) is V22() real ext-real Element of REAL
r . s is V22() real ext-real Element of REAL
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
((g - p) / x2) * (s + 1) is V22() real ext-real Element of REAL
p + (((g - p) / x2) * (s + 1)) is V22() real ext-real Element of REAL
r . (s + 1) is V22() real ext-real Element of REAL
p + 0 is V22() real ext-real Element of REAL
(r . (s + 1)) - (r . s) is V22() real ext-real Element of REAL
abs ((r . (s + 1)) - (r . s)) is V22() real ext-real Element of REAL
(p + (((g - p) / x2) * (s + 1))) - (r . s) is V22() real ext-real Element of REAL
abs ((p + (((g - p) / x2) * (s + 1))) - (r . s)) is V22() real ext-real Element of REAL
(p + (((g - p) / x2) * (s + 1))) - (p + (((g - p) / x2) * s)) is V22() real ext-real Element of REAL
abs ((p + (((g - p) / x2) * (s + 1))) - (p + (((g - p) / x2) * s))) is V22() real ext-real Element of REAL
f . (r . (s + 1)) is V22() real ext-real Element of REAL
f . (r . s) is V22() real ext-real Element of REAL
(f . (r . (s + 1))) - (f . (r . s)) is V22() real ext-real Element of REAL
abs ((f . (r . (s + 1))) - (f . (r . s))) is V22() real ext-real Element of REAL
r . x2 is V22() real ext-real Element of REAL
p + (((g - p) / x2) * x2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
r . s is V22() real ext-real Element of REAL
f . (r . s) is V22() real ext-real Element of REAL
r . 0 is V22() real ext-real Element of REAL
((g - p) / x2) * 0 is V22() real ext-real Element of REAL
p + (((g - p) / x2) * 0) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
l1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
r . l1 is V22() real ext-real Element of REAL
f . (r . l1) is V22() real ext-real Element of REAL
y - (f . (r . l1)) is V22() real ext-real Element of REAL
l1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
r . (l1 + 1) is V22() real ext-real Element of REAL
f . (r . (l1 + 1)) is V22() real ext-real Element of REAL
(f . (r . (l1 + 1))) - (f . (r . l1)) is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
abs ((f . (r . (l1 + 1))) - (f . (r . l1))) is V22() real ext-real Element of REAL
s + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
abs (y - (f . (r . l1))) is V22() real ext-real Element of REAL
K20([.p,g.],REAL) is complex-valued ext-real-valued real-valued set
K19(K20([.p,g.],REAL)) is set
[.p,g.] --> y is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
{} \/ [.(f . g),(f . p).] is V45() V46() V47() set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . g <= b₁ & b₁ <= f . p ) } is set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
x2 is V1() V4([.p,g.]) V5( REAL ) Function-like total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20([.p,g.],REAL))
s is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom s is V45() V46() V47() Element of K19(REAL)
(dom s) /\ (dom f) is V45() V46() V47() Element of K19(REAL)
s - f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) f is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
s + (- f) is V1() V4( REAL ) Function-like complex-valued ext-real-valued real-valued set
dom (s - f) is V45() V46() V47() Element of K19(REAL)
abs (s - f) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(abs (s - f)) " {0} is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
dom (abs (s - f)) is V45() V46() V47() Element of K19(REAL)
(abs (s - f)) . x1 is V22() real ext-real Element of REAL
(s - f) . x1 is V22() real ext-real Element of REAL
abs ((s - f) . x1) is V22() real ext-real Element of REAL
s . x1 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
(s . x1) - (f . x1) is V22() real ext-real Element of REAL
y - (f . x1) is V22() real ext-real Element of REAL
(abs (s - f)) ^ is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((abs (s - f)) ^) is V45() V46() V47() Element of K19(REAL)
dom (abs (s - f)) is V45() V46() V47() Element of K19(REAL)
(dom (abs (s - f))) \ ((abs (s - f)) " {0}) is V45() V46() V47() Element of K19(REAL)
[.p,g.] /\ (dom f) is V45() V46() V47() Element of K19(REAL)
[.p,g.] /\ (dom s) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
s . x1 is V22() real ext-real Element of REAL
s | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(s - f) | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(abs (s - f)) | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs (s - f)) ^) | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((abs (s - f)) ^) .: [.p,g.] is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real set
x1 is V22() real ext-real set
abs x1 is V22() real ext-real Element of REAL
(abs x1) + 1 is V22() real ext-real Element of REAL
0 + 0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() V45() V46() V47() V48() V49() V50() V51() bounded_below V69() Element of NAT
((abs x1) + 1) " is V22() real ext-real Element of REAL
1 / ((abs x1) + 1) is V22() real ext-real Element of REAL
dom (f | [.p,g.]) is V45() V46() V47() Element of K19(REAL)
x1 is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
((abs (s - f)) ^) . x2 is V22() real ext-real Element of REAL
(abs (s - f)) . x2 is V22() real ext-real Element of REAL
((abs (s - f)) . x2) " is V22() real ext-real Element of REAL
(s - f) . x2 is V22() real ext-real Element of REAL
abs ((s - f) . x2) is V22() real ext-real Element of REAL
(abs ((s - f) . x2)) " is V22() real ext-real Element of REAL
s . x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
(s . x2) - (f . x2) is V22() real ext-real Element of REAL
abs ((s . x2) - (f . x2)) is V22() real ext-real Element of REAL
(abs ((s . x2) - (f . x2))) " is V22() real ext-real Element of REAL
y - (f . x2) is V22() real ext-real Element of REAL
abs (y - (f . x2)) is V22() real ext-real Element of REAL
(abs (y - (f . x2))) " is V22() real ext-real Element of REAL
x1 + 0 is V22() real ext-real Element of REAL
1 / ((abs (y - (f . x2))) ") is V22() real ext-real Element of REAL
g - p is V22() real ext-real Element of REAL
(g - p) / x1 is V22() real ext-real Element of REAL
x2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
x1 * x2 is V22() real ext-real Element of REAL
((g - p) / x1) * x1 is V22() real ext-real Element of REAL
(x1 * x2) / x2 is V22() real ext-real Element of REAL
(g - p) / x2 is V22() real ext-real Element of REAL
x2 " is V22() real ext-real non negative Element of REAL
(x1 * x2) * (x2 ") is V22() real ext-real Element of REAL
x2 * (x2 ") is V22() real ext-real non negative Element of REAL
x1 * (x2 * (x2 ")) is V22() real ext-real Element of REAL
x1 * 1 is V22() real ext-real Element of REAL
r is V1() V4( NAT ) V5( REAL ) Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
((g - p) / x2) * x2 is V22() real ext-real Element of REAL
((g - p) / x2) * s is V22() real ext-real Element of REAL
g - (((g - p) / x2) * s) is V22() real ext-real Element of REAL
g - (g - p) is V22() real ext-real Element of REAL
r . s is V22() real ext-real Element of REAL
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
((g - p) / x2) * (s + 1) is V22() real ext-real Element of REAL
g - (((g - p) / x2) * (s + 1)) is V22() real ext-real Element of REAL
r . (s + 1) is V22() real ext-real Element of REAL
g - 0 is V22() real ext-real Element of REAL
(r . (s + 1)) - (r . s) is V22() real ext-real Element of REAL
abs ((r . (s + 1)) - (r . s)) is V22() real ext-real Element of REAL
(g - (((g - p) / x2) * (s + 1))) - (r . s) is V22() real ext-real Element of REAL
abs ((g - (((g - p) / x2) * (s + 1))) - (r . s)) is V22() real ext-real Element of REAL
(g - (((g - p) / x2) * (s + 1))) - (g - (((g - p) / x2) * s)) is V22() real ext-real Element of REAL
abs ((g - (((g - p) / x2) * (s + 1))) - (g - (((g - p) / x2) * s))) is V22() real ext-real Element of REAL
(((g - p) / x2) * (s + 1)) - (((g - p) / x2) * s) is V22() real ext-real Element of REAL
- ((((g - p) / x2) * (s + 1)) - (((g - p) / x2) * s)) is V22() real ext-real Element of REAL
abs (- ((((g - p) / x2) * (s + 1)) - (((g - p) / x2) * s))) is V22() real ext-real Element of REAL
(s + 1) - s is V22() real ext-real Element of REAL
((g - p) / x2) * ((s + 1) - s) is V22() real ext-real Element of REAL
abs (((g - p) / x2) * ((s + 1) - s)) is V22() real ext-real Element of REAL
f . (r . (s + 1)) is V22() real ext-real Element of REAL
f . (r . s) is V22() real ext-real Element of REAL
(f . (r . (s + 1))) - (f . (r . s)) is V22() real ext-real Element of REAL
abs ((f . (r . (s + 1))) - (f . (r . s))) is V22() real ext-real Element of REAL
r . x2 is V22() real ext-real Element of REAL
g - (((g - p) / x2) * x2) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
r . s is V22() real ext-real Element of REAL
f . (r . s) is V22() real ext-real Element of REAL
r . 0 is V22() real ext-real Element of REAL
((g - p) / x2) * 0 is V22() real ext-real Element of REAL
g - (((g - p) / x2) * 0) is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
s + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
l1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
r . l1 is V22() real ext-real Element of REAL
f . (r . l1) is V22() real ext-real Element of REAL
y - (f . (r . l1)) is V22() real ext-real Element of REAL
l1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() real ext-real positive non negative V33() V34() V45() V46() V47() V48() V49() V50() left_end bounded_below Element of NAT
r . (l1 + 1) is V22() real ext-real Element of REAL
f . (r . (l1 + 1)) is V22() real ext-real Element of REAL
(f . (r . (l1 + 1))) - (f . (r . l1)) is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
abs ((f . (r . (l1 + 1))) - (f . (r . l1))) is V22() real ext-real Element of REAL
s + 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() bounded_below Element of NAT
abs (y - (f . (r . l1))) is V22() real ext-real Element of REAL
{(f . p)} is non empty V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V45() V46() V47() V69() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f .: [.p,g.] is V45() V46() V47() Element of K19(REAL)
lower_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
upper_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
[.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is V45() V46() V47() V69() Element of K19(REAL)
s is V22() real ext-real set
x1 is V22() real ext-real set
f . s is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
f . x1 is V22() real ext-real Element of REAL
[.(upper_bound (f .: [.p,g.])),(lower_bound (f .: [.p,g.])).] is V45() V46() V47() V69() Element of K19(REAL)
[.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] \/ [.(upper_bound (f .: [.p,g.])),(lower_bound (f .: [.p,g.])).] is V45() V46() V47() Element of K19(REAL)
x2 is V22() real ext-real Element of REAL
[.x1,x2.] is V45() V46() V47() V69() Element of K19(REAL)
f | [.x1,x2.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
[.x2,x1.] is V45() V46() V47() V69() Element of K19(REAL)
f | [.x2,x1.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V45() V46() V47() V69() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
{p} is non empty V45() V46() V47() Element of K19(REAL)
f . p is V22() real ext-real Element of REAL
f . g is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
f . y is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . y <= b₁ & b₁ <= f . g ) } is set
[.(f . y),(f . g).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . g),(f . y).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . y),(f . g).] \/ [.(f . g),(f . y).] is V45() V46() V47() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
[.y,g.] is V45() V46() V47() V69() Element of K19(REAL)
f | [.y,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( y <= b₁ & b₁ <= g ) } is set
s is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . p <= b₁ & b₁ <= f . y ) } is set
[.(f . p),(f . y).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . y),(f . p).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . p),(f . y).] \/ [.(f . y),(f . p).] is V45() V46() V47() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
[.p,y.] is V45() V46() V47() V69() Element of K19(REAL)
f | [.p,y.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= y ) } is set
s is V22() real ext-real Element of REAL
[.p,g.] /\ (dom f) is V45() V46() V47() Element of K19(REAL)
y is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
f . y is V22() real ext-real Element of REAL
[.p,y.] is V45() V46() V47() V69() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
s is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . p <= b₁ & b₁ <= f . y ) } is set
[.(f . p),(f . y).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . y),(f . p).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . p),(f . y).] \/ [.(f . y),(f . p).] is V45() V46() V47() Element of K19(REAL)
f | [.p,y.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= y ) } is set
x1 is V22() real ext-real Element of REAL
y is V22() real ext-real Element of REAL
f . y is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . y <= b₁ & b₁ <= f . p ) } is set
[.(f . y),(f . p).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . p),(f . y).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . p),(f . y).] \/ [.(f . y),(f . p).] is V45() V46() V47() Element of K19(REAL)
[.p,y.] is V45() V46() V47() V69() Element of K19(REAL)
f | [.p,y.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= y ) } is set
s is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . g <= b₁ & b₁ <= f . y ) } is set
[.(f . g),(f . y).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . y),(f . g).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . y),(f . g).] \/ [.(f . g),(f . y).] is V45() V46() V47() Element of K19(REAL)
[.y,g.] is V45() V46() V47() V69() Element of K19(REAL)
f | [.y,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( y <= b₁ & b₁ <= g ) } is set
s is V22() real ext-real Element of REAL
[.p,g.] /\ (dom f) is V45() V46() V47() Element of K19(REAL)
y is V22() real ext-real Element of REAL
x2 is V22() real ext-real Element of REAL
f . y is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
[.x2,g.] is V45() V46() V47() V69() Element of K19(REAL)
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
s is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( f . g <= b₁ & b₁ <= f . x2 ) } is set
[.(f . g),(f . x2).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . x2),(f . g).] is V45() V46() V47() V69() Element of K19(REAL)
[.(f . x2),(f . g).] \/ [.(f . g),(f . x2).] is V45() V46() V47() Element of K19(REAL)
f | [.x2,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
f . s is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( x2 <= b₁ & b₁ <= g ) } is set
x1 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V45() V46() V47() V69() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f .: [.p,g.] is V45() V46() V47() Element of K19(REAL)
lower_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
f . p is V22() real ext-real Element of REAL
upper_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
f . g is V22() real ext-real Element of REAL
[.p,g.] /\ (dom f) is V45() V46() V47() Element of K19(REAL)
y is V22() real ext-real set
x2 is V22() real ext-real set
f . y is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( p <= b₁ & b₁ <= g ) } is set
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V45() V46() V47() V69() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f .: [.p,g.] is V45() V46() V47() Element of K19(REAL)
lower_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
upper_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
[.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is V45() V46() V47() V69() Element of K19(REAL)
y is V22() real ext-real Element of REAL
{ b₁ where b₁ is V22() real ext-real Element of REAL : ( lower_bound (f .: [.p,g.]) <= b₁ & b₁ <= upper_bound (f .: [.p,g.]) ) } is set
x2 is V22() real ext-real Element of REAL
f . x2 is V22() real ext-real Element of REAL
p is V22() real ext-real Element of REAL
g is V22() real ext-real Element of REAL
[.p,g.] is V45() V46() V47() V69() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) Function-like one-to-one complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom f is V45() V46() V47() Element of K19(REAL)
f | [.p,g.] is V1() V4( REAL ) V5( REAL ) Function-like one-to-one complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f " is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
f .: [.p,g.] is V45() V46() V47() Element of K19(REAL)
lower_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
upper_bound (f .: [.p,g.]) is V22() real ext-real Element of REAL
[.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is V45() V46() V47() V69() Element of K19(REAL)
(f ") | [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f | [.p,g.]) " is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f | [.p,g.]) ") | (f .: [.p,g.]) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f ") | (f .: [.p,g.]) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is V45() V46() V47() Element of K19(REAL)
(f ") .: (f .: [.p,g.]) is V45() V46() V47() Element of K19(REAL)
((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) is V45() V46() V47() Element of K19(REAL)
((f | [.p,g.]) ") .: (f .: [.p,g.]) is V45() V46() V47() Element of K19(REAL)
rng (f | [.p,g.]) is V45() V46() V47() Element of K19(REAL)
((f | [.p,g.]) ") .: (rng (f | [.p,g.])) is V45() V46() V47() Element of K19(REAL)
dom ((f | [.p,g.]) ") is V45() V46() V47() Element of K19(REAL)
((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) is V45() V46() V47() Element of K19(REAL)
rng ((f | [.p,g.]) ") is V45() V46() V47() Element of K19(REAL)
dom (f | [.p,g.]) is V45() V46() V47() Element of K19(REAL)
(dom f) /\ [.p,g.] is V45() V46() V47() Element of K19(REAL)
(f | [.p,g.]) " is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f | [.p,g.]) ") | (f .: [.p,g.]) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f ") | (f .: [.p,g.]) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((f ") | (f .: [.p,g.])) | (f .: [.p,g.]) is V1() V4( REAL ) V5( REAL ) Function-like complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(f ") .: [.(lower_bound (f .: [.p,g.])),(upper_bound (f .: [.p,g.])).] is V45() V46() V47() Element of K19(REAL)
(f ") .: (f .: [.p,g.]) is V45() V46() V47() Element of K19(REAL)
((f ") | (f .: [.p,g.])) .: (f .: [.p,g.]) is V45() V46() V47() Element of K19(REAL)
((f | [.p,g.]) ") .: (f .: [.p,g.]) is V45() V46() V47() Element of K19(REAL)
rng (f | [.p,g.]) is V45() V46() V47() Element of K19(REAL)
((f | [.p,g.]) ") .: (rng (f | [.p,g.])) is V45() V46() V47() Element of K19(REAL)
dom ((f | [.p,g.]) ") is V45() V46() V47() Element of K19(REAL)
((f | [.p,g.]) ") .: (dom ((f | [.p,g.]) ")) is V45() V46() V47() Element of K19(REAL)
rng ((f | [.p,g.]) ") is V45() V46() V47() Element of K19(REAL)
dom (f | [.p,g.]) is V45() V46() V47() Element of K19(REAL)
(dom f) /\ [.p,g.] is V45() V46() V47() Element of K19(REAL)