:: RCOMP_1 semantic presentation

REAL is non empty V50() V51() V52() V56() V57() non bounded_below non bounded_above V71() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() left_end bounded_below Element of K19(REAL)

K19(REAL) is set

COMPLEX is non empty V50() V56() V57() set

RAT is non empty V50() V51() V52() V53() V56() V57() set

INT is non empty V50() V51() V52() V53() V54() V56() V57() set

omega is non empty epsilon-transitive epsilon-connected ordinal V50() V51() V52() V53() V54() V55() V56() 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

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 RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(RAT,RAT)) is set

K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(RAT,RAT),RAT)) is set

K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(INT,INT)) is set

K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set

K19(K20(K20(INT,INT),INT)) is set

K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(K20(NAT,NAT),NAT)) is set

{} is set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V50() V51() V52() V53() V54() V55() V56() bounded_below V71() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V50() V51() V52() V53() V54() V55() V56() bounded_below V71() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

K20(NAT,REAL) is complex-valued ext-real-valued real-valued set

K19(K20(NAT,REAL)) is set

0 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

K19(K20(NAT,NAT)) is set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

ExtREAL is non empty V51() V71() set

g is V30() real ext-real set

s is V30() real ext-real set

[.g,s.] is V71() set

{ b

Y is set

X is ext-real Element of ExtREAL

{ b

X is V50() V51() V52() Element of K19(REAL)

e is set

r is ext-real Element of ExtREAL

e is set

r is V30() real ext-real Element of REAL

g is ext-real set

s is ext-real set

].g,s.[ is non left_end non right_end V71() set

{ b

Y is set

X is ext-real Element of ExtREAL

{ b

X is V50() V51() V52() Element of K19(REAL)

e is set

r is V30() real ext-real Element of REAL

e is set

r is ext-real Element of ExtREAL

g is V30() real ext-real set

s is V30() real ext-real set

g - s is V30() real ext-real set

abs (g - s) is V30() real ext-real Element of REAL

Y is V30() real ext-real set

s - Y is V30() real ext-real set

s + Y is V30() real ext-real set

((s - Y),(s + Y)) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)

{ b

{ b

- Y is V30() real ext-real set

s + (- Y) is V30() real ext-real set

X is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

- Y is V30() real ext-real set

s + (- Y) is V30() real ext-real set

g is V30() real ext-real set

2 * g is V30() real ext-real Element of REAL

s is V30() real ext-real set

Y is V30() real ext-real set

(s,Y) is V50() V51() V52() V71() Element of K19(REAL)

{ b

{ b

s + Y is V30() real ext-real set

(s + Y) - (2 * g) is V30() real ext-real Element of REAL

abs ((s + Y) - (2 * g)) is V30() real ext-real Element of REAL

Y - s is V30() real ext-real set

2 * Y is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

- (2 * Y) is V30() real ext-real Element of REAL

- (2 * g) is V30() real ext-real Element of REAL

(s + Y) + (- (2 * Y)) is V30() real ext-real Element of REAL

(s + Y) + (- (2 * g)) is V30() real ext-real Element of REAL

- (Y - s) is V30() real ext-real set

2 * s is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

- (2 * s) is V30() real ext-real Element of REAL

(s + Y) + (- (2 * s)) is V30() real ext-real Element of REAL

- (Y - s) is V30() real ext-real set

s - Y is V30() real ext-real set

(s - Y) + (2 * g) is V30() real ext-real Element of REAL

(s + Y) - (s - Y) is V30() real ext-real set

1 / 2 is V30() real ext-real non negative Element of REAL

(1 / 2) * (2 * g) is V30() real ext-real Element of REAL

2 * Y is V30() real ext-real Element of REAL

(1 / 2) * (2 * Y) is V30() real ext-real Element of REAL

(2 * g) + (Y - s) is V30() real ext-real Element of REAL

(s + Y) - (Y - s) is V30() real ext-real set

2 * s is V30() real ext-real Element of REAL

(1 / 2) * (2 * s) is V30() real ext-real Element of REAL

g is V30() real ext-real set

2 * g is V30() real ext-real Element of REAL

s is V30() real ext-real set

Y is V30() real ext-real set

(s,Y) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)

{ b

{ b

Y - s is V30() real ext-real set

s + Y is V30() real ext-real set

(s + Y) - (2 * g) is V30() real ext-real Element of REAL

abs ((s + Y) - (2 * g)) is V30() real ext-real Element of REAL

2 * Y is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

- (2 * g) is V30() real ext-real Element of REAL

- (2 * Y) is V30() real ext-real Element of REAL

(s + Y) + (- (2 * g)) is V30() real ext-real Element of REAL

(s + Y) + (- (2 * Y)) is V30() real ext-real Element of REAL

- (Y - s) is V30() real ext-real set

2 * s is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

- (2 * s) is V30() real ext-real Element of REAL

(s + Y) + (- (2 * s)) is V30() real ext-real Element of REAL

- (Y - s) is V30() real ext-real set

s - Y is V30() real ext-real set

(s - Y) + (2 * g) is V30() real ext-real Element of REAL

(s + Y) - (s - Y) is V30() real ext-real set

1 / 2 is V30() real ext-real non negative Element of REAL

2 * Y is V30() real ext-real Element of REAL

(1 / 2) * (2 * Y) is V30() real ext-real Element of REAL

(1 / 2) * (2 * g) is V30() real ext-real Element of REAL

(2 * g) + (Y - s) is V30() real ext-real Element of REAL

(s + Y) - (Y - s) is V30() real ext-real set

2 * s is V30() real ext-real Element of REAL

(1 / 2) * (2 * s) is V30() real ext-real Element of REAL

g is V30() real ext-real set

s is V30() real ext-real set

(g,s) is V50() V51() V52() V71() Element of K19(REAL)

{ b

{ b

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng Y is V50() V51() V52() set

s + 1 is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

e is V30() real ext-real set

r is V30() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . e is V30() real ext-real Element of REAL

dom Y is set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . e is V30() real ext-real Element of REAL

g - 1 is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

X + 1 is V30() real ext-real Element of REAL

1 - 1 is V30() real ext-real Element of REAL

g - (1 - 1) is V30() real ext-real Element of REAL

e is V30() real ext-real set

r is V30() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . e is V30() real ext-real Element of REAL

dom Y is set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . e is V30() real ext-real Element of REAL

g is V30() real ext-real set

s is V30() real ext-real set

(g,s) is V50() V51() V52() V71() Element of K19(REAL)

{ b

{ b

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng Y is V50() V51() V52() set

lim Y is V30() real ext-real Element of REAL

NAT --> g is Relation-like NAT -defined {g} -valued V6() constant non empty V14( NAT ) V18( NAT ,{g}) T-Sequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{g}))

{g} is V50() V51() V52() set

K20(NAT,{g}) is complex-valued ext-real-valued real-valued set

K19(K20(NAT,{g})) is set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

dom Y is set

Y . e is V30() real ext-real Element of REAL

X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

X . e is V30() real ext-real Element of REAL

r is V30() real ext-real Element of REAL

X . 0 is V30() real ext-real Element of REAL

lim X is V30() real ext-real Element of REAL

NAT --> s is Relation-like NAT -defined {s} -valued V6() constant non empty V14( NAT ) V18( NAT ,{s}) T-Sequence-like complex-valued ext-real-valued real-valued Element of K19(K20(NAT,{s}))

{s} is V50() V51() V52() set

K20(NAT,{s}) is complex-valued ext-real-valued real-valued set

K19(K20(NAT,{s})) is set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

dom Y is set

Y . e is V30() real ext-real Element of REAL

X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

X . e is V30() real ext-real Element of REAL

r is V30() real ext-real Element of REAL

X . 0 is V30() real ext-real Element of REAL

lim X is V30() real ext-real Element of REAL

g is V30() real ext-real set

s is V30() real ext-real set

(g,s) is V50() V51() V52() V71() Element of K19(REAL)

{ b

{ b

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng Y is V50() V51() V52() set

X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim X is V30() real ext-real Element of REAL

rng X is V50() V51() V52() set

e is Relation-like NAT -defined NAT -valued V6() non empty V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

Y * e is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of Y

g is V30() real ext-real set

s is V30() real ext-real set

(g,s) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)

{ b

{ b

Y is V50() V51() V52() Element of K19(REAL)

X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng X is V50() V51() V52() set

lim X is V30() real ext-real Element of REAL

(lim X) - g is V30() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s - (lim X) is V30() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

max (r,e) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative set

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

X . g1 is V30() real ext-real Element of REAL

(X . g1) - (lim X) is V30() real ext-real Element of REAL

abs ((X . g1) - (lim X)) is V30() real ext-real Element of REAL

- (abs ((X . g1) - (lim X))) is V30() real ext-real Element of REAL

- ((X . g1) - (lim X)) is V30() real ext-real Element of REAL

- (- (abs ((X . g1) - (lim X)))) is V30() real ext-real Element of REAL

- (- ((X . g1) - (lim X))) is V30() real ext-real Element of REAL

- ((lim X) - g) is V30() real ext-real Element of REAL

g - (lim X) is V30() real ext-real Element of REAL

dom X is set

X is V30() real ext-real set

(g,s) ` is V50() V51() V52() Element of K19(REAL)

REAL \ (g,s) is V50() V51() V52() set

X is V30() real ext-real set

e is V30() real ext-real Element of REAL

g is V30() real ext-real set

s is V30() real ext-real set

(g,s) is V50() V51() V52() non left_end non right_end V71() Element of K19(REAL)

{ b

{ b

Y is V50() V51() V52() Element of K19(REAL)

(g,s) is V50() V51() V52() V71() Element of K19(REAL)

{ b

{ b

Y is V50() V51() V52() Element of K19(REAL)

g is V50() V51() V52() Element of K19(REAL)

s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng s is V50() V51() V52() set

lim s is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim Y is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

g is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

s is V50() V51() V52() Element of K19(REAL)

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim Y is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim Y is V30() real ext-real Element of REAL

X is V30() real ext-real set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g1 is Relation-like NAT -defined NAT -valued V6() non empty V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

g * g1 is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of g

e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

(e + 1) + r is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

(g * g1) . ((e + 1) + r) is V30() real ext-real Element of REAL

((g * g1) . ((e + 1) + r)) - (lim Y) is V30() real ext-real Element of REAL

abs (((g * g1) . ((e + 1) + r)) - (lim Y)) is V30() real ext-real Element of REAL

g1 . ((e + 1) + r) is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g . (g1 . ((e + 1) + r)) is V30() real ext-real Element of REAL

(g . (g1 . ((e + 1) + r))) - (lim Y) is V30() real ext-real Element of REAL

abs ((g . (g1 . ((e + 1) + r))) - (lim Y)) is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y is ext-real set

s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . Y is V30() real ext-real Element of REAL

X is V30() real ext-real set

Y is V30() real ext-real set

X is V30() real ext-real set

e is V30() real ext-real set

Y + 1 is V30() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . g2 is V30() real ext-real Element of REAL

(s . g2) - Y is V30() real ext-real Element of REAL

abs ((s . g2) - Y) is V30() real ext-real Element of REAL

rng s is V50() V51() V52() set

Y is set

dom s is set

X is set

s . X is V30() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . e is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim Y is V30() real ext-real Element of REAL

s is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

- s is V30() real ext-real non positive Element of REAL

Y is ext-real set

s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . Y is V30() real ext-real Element of REAL

- Y is V30() real ext-real non positive Element of REAL

X is V30() real ext-real set

Y is V30() real ext-real set

X is V30() real ext-real set

e is V30() real ext-real set

Y - 1 is V30() real ext-real Element of REAL

abs (Y - 1) is V30() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . g2 is V30() real ext-real Element of REAL

(s . g2) - Y is V30() real ext-real Element of REAL

abs ((s . g2) - Y) is V30() real ext-real Element of REAL

- g1 is V30() real ext-real non positive Element of REAL

- g2 is V30() real ext-real non positive Element of REAL

- r is V30() real ext-real non positive Element of REAL

(s . g2) + 1 is V30() real ext-real Element of REAL

Y - (s . g2) is V30() real ext-real Element of REAL

- ((s . g2) - Y) is V30() real ext-real Element of REAL

abs (- ((s . g2) - Y)) is V30() real ext-real Element of REAL

rng s is V50() V51() V52() set

Y is set

dom s is set

X is set

s . X is V30() real ext-real Element of REAL

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . e is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

lim Y is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng s is V50() V51() V52() set

Y is V30() real ext-real set

X is V30() real ext-real set

Y - 1 is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

X + 1 is V30() real ext-real Element of REAL

1 - 1 is V30() real ext-real Element of REAL

Y - (1 - 1) is V30() real ext-real Element of REAL

e is V30() real ext-real set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . e is V30() real ext-real Element of REAL

dom s is set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . e is V30() real ext-real Element of REAL

Y is V30() real ext-real set

X is V30() real ext-real set

Y + 1 is V30() real ext-real Element of REAL

X is V30() real ext-real Element of REAL

e is V30() real ext-real set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . e is V30() real ext-real Element of REAL

dom s is set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

s . e is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng Y is V50() V51() V52() set

X is Relation-like NAT -defined NAT -valued V6() non empty V14( NAT ) V18( NAT , NAT ) complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of K19(K20(NAT,NAT))

s * X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued subsequence of s

lim Y is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

upper_bound g is V30() real ext-real Element of REAL

Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (Y + 1) is V30() real ext-real non negative Element of REAL

(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL

(upper_bound g) - (1 / (Y + 1)) is V30() real ext-real Element of REAL

X is V30() real ext-real set

X + (1 / (Y + 1)) is V30() real ext-real Element of REAL

(upper_bound g) - X is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

X is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . X is V30() real ext-real Element of REAL

X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (X + 1) is V30() real ext-real non negative Element of REAL

(upper_bound g) - (Y . X) is V30() real ext-real Element of REAL

e is V30() real ext-real set

(upper_bound g) - e is V30() real ext-real Element of REAL

rng Y is V50() V51() V52() set

X is set

dom Y is set

e is set

Y . e is V30() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . r is V30() real ext-real Element of REAL

X is V30() real ext-real set

X " is V30() real ext-real set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

g1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (g1 + 1) is V30() real ext-real non negative Element of REAL

1 / (r + 1) is V30() real ext-real non negative Element of REAL

Y . g1 is V30() real ext-real Element of REAL

(upper_bound g) - (Y . g1) is V30() real ext-real Element of REAL

e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

(X ") + 0 is V30() real ext-real Element of REAL

1 / (X ") is V30() real ext-real Element of REAL

1 / (e + 1) is V30() real ext-real non negative Element of REAL

(Y . g1) - (upper_bound g) is V30() real ext-real Element of REAL

- ((Y . g1) - (upper_bound g)) is V30() real ext-real Element of REAL

abs (- ((Y . g1) - (upper_bound g))) is V30() real ext-real Element of REAL

abs ((Y . g1) - (upper_bound g)) is V30() real ext-real Element of REAL

lim Y is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

lower_bound g is V30() real ext-real Element of REAL

Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (Y + 1) is V30() real ext-real non negative Element of REAL

(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL

(lower_bound g) + (1 / (Y + 1)) is V30() real ext-real Element of REAL

X is V30() real ext-real set

X - (lower_bound g) is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

X is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . X is V30() real ext-real Element of REAL

X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (X + 1) is V30() real ext-real non negative Element of REAL

(Y . X) - (lower_bound g) is V30() real ext-real Element of REAL

e is V30() real ext-real set

e - (lower_bound g) is V30() real ext-real Element of REAL

rng Y is V50() V51() V52() set

X is set

dom Y is set

e is set

Y . e is V30() real ext-real Element of REAL

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . r is V30() real ext-real Element of REAL

X is V30() real ext-real set

X " is V30() real ext-real set

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

g1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (g1 + 1) is V30() real ext-real non negative Element of REAL

1 / (r + 1) is V30() real ext-real non negative Element of REAL

Y . g1 is V30() real ext-real Element of REAL

(Y . g1) - (lower_bound g) is V30() real ext-real Element of REAL

e + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

(X ") + 0 is V30() real ext-real Element of REAL

1 / (X ") is V30() real ext-real Element of REAL

1 / (e + 1) is V30() real ext-real non negative Element of REAL

abs ((Y . g1) - (lower_bound g)) is V30() real ext-real Element of REAL

lim Y is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

upper_bound g is V30() real ext-real Element of REAL

lower_bound g is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

(1,0) is V50() V51() V52() V71() () Element of K19(REAL)

{ b

{ b

lower_bound g is V30() real ext-real Element of REAL

s is V30() real ext-real Element of REAL

upper_bound g is V30() real ext-real Element of REAL

Y is V30() real ext-real Element of REAL

(s,Y) is V50() V51() V52() V71() () Element of K19(REAL)

{ b

{ b

X is V30() real ext-real Element of REAL

(0,1) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g is V30() real ext-real set

g - 1 is V30() real ext-real Element of REAL

g + 1 is V30() real ext-real Element of REAL

((g - 1),(g + 1)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g is V30() real ext-real set

s is V50() V51() V52() (g)

Y is V30() real ext-real set

g - Y is V30() real ext-real set

g + Y is V30() real ext-real set

((g - Y),(g + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g is V30() real ext-real set

s is V50() V51() V52() () (g)

g - g is V30() real ext-real set

abs (g - g) is V30() real ext-real Element of REAL

Y is V30() real ext-real set

g - Y is V30() real ext-real set

g + Y is V30() real ext-real set

((g - Y),(g + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g is V30() real ext-real set

s is V50() V51() V52() () (g)

Y is V50() V51() V52() () (g)

X is V30() real ext-real set

g - X is V30() real ext-real set

g + X is V30() real ext-real set

((g - X),(g + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

e is V30() real ext-real set

g - e is V30() real ext-real set

g + e is V30() real ext-real set

((g - e),(g + e)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

min (X,e) is V30() real ext-real set

g - (min (X,e)) is V30() real ext-real set

g + (min (X,e)) is V30() real ext-real set

((g - (min (X,e))),(g + (min (X,e)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g1 is V50() V51() V52() () (g)

- X is V30() real ext-real set

- (min (X,e)) is V30() real ext-real set

g + (- X) is V30() real ext-real set

g + (- (min (X,e))) is V30() real ext-real set

- e is V30() real ext-real set

g + (- e) is V30() real ext-real set

g2 is set

m is V30() real ext-real Element of REAL

c

g2 is set

m is V30() real ext-real Element of REAL

c

g is V50() V51() V52() () Element of K19(REAL)

s is V30() real ext-real set

g ` is V50() V51() V52() Element of K19(REAL)

REAL \ g is V50() V51() V52() set

Y is V50() V51() V52() () (s)

X is V30() real ext-real set

s - X is V30() real ext-real set

s + X is V30() real ext-real set

((s - X),(s + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

e is set

r is V30() real ext-real Element of REAL

g1 is V30() real ext-real Element of REAL

Y is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (Y + 1) is V30() real ext-real non negative Element of REAL

s - (1 / (Y + 1)) is V30() real ext-real Element of REAL

s + (1 / (Y + 1)) is V30() real ext-real Element of REAL

((s - (1 / (Y + 1))),(s + (1 / (Y + 1)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

(Y + 1) " is non empty V30() real ext-real positive non negative Element of REAL

1 * ((Y + 1) ") is V30() real ext-real non negative Element of REAL

X is V50() V51() V52() () (s)

e is V30() real ext-real Element of REAL

Y is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

X is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

e is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

X . r is V30() real ext-real Element of REAL

Y . r is V30() real ext-real Element of REAL

e . r is V30() real ext-real Element of REAL

r + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (r + 1) is V30() real ext-real non negative Element of REAL

s - (1 / (r + 1)) is V30() real ext-real Element of REAL

s + (1 / (r + 1)) is V30() real ext-real Element of REAL

((s - (1 / (r + 1))),(s + (1 / (r + 1)))) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g1 is V30() real ext-real Element of REAL

g1 is V30() real ext-real Element of REAL

rng Y is V50() V51() V52() set

r is set

dom Y is set

g1 is set

Y . g1 is V30() real ext-real Element of REAL

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

Y . g2 is V30() real ext-real Element of REAL

r is V30() real ext-real set

r " is V30() real ext-real set

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (m + 1) is V30() real ext-real non negative Element of REAL

1 / (g2 + 1) is V30() real ext-real non negative Element of REAL

(r ") + 0 is V30() real ext-real Element of REAL

1 / (r ") is V30() real ext-real Element of REAL

e . m is V30() real ext-real Element of REAL

(e . m) - s is V30() real ext-real Element of REAL

abs ((e . m) - s) is V30() real ext-real Element of REAL

s + (1 / (m + 1)) is V30() real ext-real Element of REAL

(s + (1 / (m + 1))) - s is V30() real ext-real Element of REAL

abs ((s + (1 / (m + 1))) - s) is V30() real ext-real Element of REAL

lim e is V30() real ext-real Element of REAL

r is V30() real ext-real set

r " is V30() real ext-real set

g1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g2 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

g2 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

m + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V48() V49() V50() V51() V52() V53() V54() V55() left_end bounded_below Element of NAT

1 / (m + 1) is V30() real ext-real non negative Element of REAL

1 / (g2 + 1) is V30() real ext-real non negative Element of REAL

(r ") + 0 is V30() real ext-real Element of REAL

1 / (r ") is V30() real ext-real Element of REAL

X . m is V30() real ext-real Element of REAL

(X . m) - s is V30() real ext-real Element of REAL

abs ((X . m) - s) is V30() real ext-real Element of REAL

s - (1 / (m + 1)) is V30() real ext-real Element of REAL

(s - (1 / (m + 1))) - s is V30() real ext-real Element of REAL

abs ((s - (1 / (m + 1))) - s) is V30() real ext-real Element of REAL

- (1 / (m + 1)) is V30() real ext-real non positive Element of REAL

abs (- (1 / (m + 1))) is V30() real ext-real Element of REAL

abs (1 / (m + 1)) is V30() real ext-real Element of REAL

lim X is V30() real ext-real Element of REAL

lim Y is V30() real ext-real Element of REAL

g is V50() V51() V52() () Element of K19(REAL)

s is V30() real ext-real set

Y is V50() V51() V52() () (s)

X is V30() real ext-real set

s - X is V30() real ext-real set

s + X is V30() real ext-real set

((s - X),(s + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

g is V50() V51() V52() Element of K19(REAL)

g ` is V50() V51() V52() Element of K19(REAL)

REAL \ g is V50() V51() V52() set

s is Relation-like NAT -defined REAL -valued V6() non empty V14( NAT ) V18( NAT , REAL ) complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))

rng s is V50() V51() V52() set

lim s is V30() real ext-real Element of REAL

Y is V50() V51() V52() () ( lim s)

X is V30() real ext-real set

(lim s) - X is V30() real ext-real Element of REAL

(lim s) + X is V30() real ext-real Element of REAL

(((lim s) - X),((lim s) + X)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

e is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real non negative V48() V49() V50() V51() V52() V53() V54() V55() bounded_below Element of NAT

dom s is set

s . e is V30() real ext-real Element of REAL

(s . e) - (lim s) is V30() real ext-real Element of REAL

abs ((s . e) - (lim s)) is V30() real ext-real Element of REAL

- X is V30() real ext-real set

(lim s) + ((s . e) - (lim s)) is V30() real ext-real Element of REAL

(lim s) + (- X) is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

upper_bound g is V30() real ext-real Element of REAL

s is V50() V51() V52() () ( upper_bound g)

Y is V30() real ext-real set

(upper_bound g) - Y is V30() real ext-real Element of REAL

(upper_bound g) + Y is V30() real ext-real Element of REAL

(((upper_bound g) - Y),((upper_bound g) + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

Y / 2 is V30() real ext-real Element of REAL

(upper_bound g) + (Y / 2) is V30() real ext-real Element of REAL

((upper_bound g) + (Y / 2)) + (Y / 2) is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

lower_bound g is V30() real ext-real Element of REAL

s is V50() V51() V52() () ( lower_bound g)

Y is V30() real ext-real set

(lower_bound g) - Y is V30() real ext-real Element of REAL

(lower_bound g) + Y is V30() real ext-real Element of REAL

(((lower_bound g) - Y),((lower_bound g) + Y)) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

Y / 2 is V30() real ext-real Element of REAL

(lower_bound g) - (Y / 2) is V30() real ext-real Element of REAL

((lower_bound g) - (Y / 2)) - (Y / 2) is V30() real ext-real Element of REAL

g is V50() V51() V52() Element of K19(REAL)

(1,0) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

lower_bound g is V30() real ext-real Element of REAL

s is V30() real ext-real Element of REAL

upper_bound g is V30() real ext-real Element of REAL

Y is V30() real ext-real Element of REAL

(s,Y) is V50() V51() V52() non left_end non right_end V71() () Element of K19(REAL)

{ b

{ b

X is V30() real ext-real Element of REAL

Y - X is V30() real ext-real Element of REAL

e is V30() real ext-real Element of REAL

Y - (Y - X) is V30() real ext-real Element of REAL

e is V30() real ext-real set

X - s is V30() real ext-real Element of REAL

r is V30() real ext-real Element of REAL

s + (X - s) is V30() real ext-real Element of REAL

r is V30() real ext-real set

g1 is V30() real ext-real Element of REAL

g2 is V30() real ext-real Element of REAL

{ b

(g1,g2) is V50() V51() V52() V71() () Element of K19(REAL)

{ b

g is V30() real ext-real set

s is ext-real set

[.g,s.[ is non right_end V71() set

{ b

Y is set

X is ext-real Element of ExtREAL

{ b

X is V50() V51() V52() Element of K19(REAL)

e is set

r is ext-real Element of ExtREAL

e is set

r is V30() real ext-real Element of REAL

g is ext-real set

s is V30() real ext-real set

].g,s.] is non left_end V71() set

{ b

Y is set

X is ext-real Element of ExtREAL

{ b

X is V50() V51() V52() Element of K19(REAL)

e is set

r is ext-real Element of ExtREAL

e is set

r is V30() real ext-real Element of REAL