REAL is non empty V45() V46() V47() V51() V52() V66() V67() V69() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V45() V46() V47() V48() V49() V50() V51() V64() V66() Element of bool REAL
bool 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() V64() V66() set
bool omega is set
bool NAT is set
[:COMPLEX,COMPLEX:] is Relation-like complex-valued set
bool [:COMPLEX,COMPLEX:] is set
[:COMPLEX,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:COMPLEX,REAL:] is set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded set
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded 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() V64() V66() Element of NAT
{{},1} is non empty V45() V46() V47() V48() V49() V50() V64() V66() set
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded Element of NAT
[:NAT,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is set
{0} is functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() set
[:REAL,REAL:] is Relation-like complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is set
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() V64() V66() Element of NAT
a is set
b is V22() real ext-real set
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
dom (u | a) is V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
(u | a) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(u | a) . b is V22() real ext-real Element of REAL
lim ((u | a) /* r) is V22() real ext-real Element of REAL
dom (u | a) is Element of bool a
bool a is set
dom u is V45() V46() V47() Element of bool REAL
a /\ (dom u) is V45() V46() V47() Element of bool REAL
u /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
u . b is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
b . a is V22() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* u) is V22() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* u) 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() V66() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u ^\ r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of u
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
(u ^\ r) . s is V22() real ext-real Element of REAL
s + r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . (s + r) is V22() real ext-real Element of REAL
b /* (u ^\ r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* u) ^\ r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of b /* u
rng (u ^\ r) is non empty V45() V46() V47() Element of bool REAL
s is V22() real ext-real set
r1 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded Element of NAT
r2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
(b /* (u ^\ r)) . r2 is V22() real ext-real Element of REAL
((b /* (u ^\ r)) . r2) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* (u ^\ r)) . r2) - (b . a)) is V22() real ext-real Element of REAL
(u ^\ r) . r2 is V22() real ext-real Element of REAL
b . ((u ^\ r) . r2) is V22() real ext-real Element of REAL
(b . ((u ^\ r) . r2)) - (b . a) is V22() real ext-real Element of REAL
abs ((b . ((u ^\ r) . r2)) - (b . a)) is V22() real ext-real Element of REAL
(b . a) - (b . a) is V22() real ext-real Element of REAL
abs ((b . a) - (b . a)) is V22() real ext-real Element of REAL
lim ((b /* u) ^\ r) 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() V66() Element of NAT
u . r is V22() real ext-real Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
u . r is V22() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r1 + 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() V64() V66() Element of NAT
r2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . r2 is V22() real ext-real Element of REAL
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . x0 is V22() real ext-real Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . x0 is V22() real ext-real Element of REAL
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
u . x0 is V22() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . N is V22() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . N is V22() real ext-real Element of REAL
[:NAT,NAT:] is Relation-like RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,NAT:] is set
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r1 is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,NAT:]
r1 . 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
rng r1 is non empty V45() V46() V47() V48() V49() V50() V64() V66() Element of bool NAT
dom r1 is non empty V45() V46() V47() V48() V49() V50() V64() V66() Element of bool NAT
r2 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r2 . x0 is V22() real ext-real Element of REAL
rng r2 is non empty V45() V46() V47() Element of bool REAL
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r2 . x0 is V22() real ext-real Element of REAL
x0 + 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() V64() V66() Element of NAT
r2 . (x0 + 1) is V22() real ext-real Element of REAL
x0 is Relation-like NAT -defined NAT -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued increasing non-decreasing Element of bool [:NAT,NAT:]
u * x0 is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued subsequence of u
lim (u * x0) is V22() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . N1 is V22() real ext-real Element of REAL
N1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
u . N1 is V22() real ext-real Element of REAL
x0 . 0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
u . N is V22() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative set
u . N is V22() real ext-real Element of REAL
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . N 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() V66() Element of NAT
x0 . R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . x1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N + 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() V64() V66() Element of NAT
x0 . (N + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . (x0 . (N + 1)) 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() V66() Element of NAT
x0 . R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
(u * x0) . N1 is V22() real ext-real Element of REAL
N1 + 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() V64() V66() Element of NAT
(u * x0) . (N1 + 1) is V22() real ext-real Element of REAL
x0 . N1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . (N1 + 1) is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . N 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() V66() Element of NAT
u . R is V22() real ext-real Element of REAL
u . (x0 . (N1 + 1)) is V22() real ext-real Element of REAL
(u * x0) . 0 is V22() real ext-real Element of REAL
rng (u * x0) is non empty V45() V46() V47() Element of bool REAL
b /* (u * x0) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* (u * x0)) is V22() real ext-real Element of REAL
N1 is V22() real ext-real set
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
N is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
R is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . R is V22() real ext-real Element of REAL
(b /* u) . R is V22() real ext-real Element of REAL
((b /* u) . R) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* u) . R) - (b . a)) is V22() real ext-real Element of REAL
(b . a) - (b . a) is V22() real ext-real Element of REAL
abs ((b . a) - (b . a)) is V22() real ext-real Element of REAL
u . R is V22() real ext-real Element of REAL
x1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 . x1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
(b /* (u * x0)) . x1 is V22() real ext-real Element of REAL
((b /* (u * x0)) . x1) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* (u * x0)) . x1) - (b . a)) is V22() real ext-real Element of REAL
(u * x0) . x1 is V22() real ext-real Element of REAL
b . ((u * x0) . x1) is V22() real ext-real Element of REAL
(b . ((u * x0) . x1)) - (b . a) is V22() real ext-real Element of REAL
abs ((b . ((u * x0) . x1)) - (b . a)) is V22() real ext-real Element of REAL
b . (u . R) is V22() real ext-real Element of REAL
(b . (u . R)) - (b . a) is V22() real ext-real Element of REAL
abs ((b . (u . R)) - (b . a)) is V22() real ext-real Element of REAL
(b /* u) . R is V22() real ext-real Element of REAL
((b /* u) . R) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* u) . R) - (b . a)) is V22() real ext-real Element of REAL
u . R is V22() real ext-real Element of REAL
(b /* u) . R is V22() real ext-real Element of REAL
((b /* u) . R) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* u) . R) - (b . a)) is V22() real ext-real Element of REAL
(b /* u) . R is V22() real ext-real Element of REAL
((b /* u) . R) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* u) . R) - (b . a)) 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() V66() Element of NAT
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
b . a is V22() real ext-real Element of REAL
u 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() V66() Element of NAT
r + 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() V64() V66() Element of NAT
1 / (r + 1) is V22() real ext-real non negative Element of REAL
(r + 1) " is non empty V22() real ext-real positive non negative Element of REAL
s is V22() real ext-real set
s - a is V22() real ext-real set
abs (s - a) is V22() real ext-real Element of REAL
b . s is V22() real ext-real Element of REAL
(b . s) - (b . a) is V22() real ext-real Element of REAL
abs ((b . s) - (b . a)) is V22() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
s is set
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r . r1 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() V66() Element of NAT
r . s is V22() real ext-real Element of REAL
b . (r . s) is V22() real ext-real Element of REAL
(b . (r . s)) - (b . a) is V22() real ext-real Element of REAL
abs ((b . (r . s)) - (b . a)) is V22() real ext-real Element of REAL
b /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* r) . s is V22() real ext-real Element of REAL
((b /* r) . s) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* r) . s) - (b . a)) is V22() real ext-real Element of REAL
s is V22() real ext-real set
s " is V22() real ext-real set
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r1 + 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() V64() V66() Element of NAT
(s ") + 0 is V22() real ext-real set
1 / (s ") is V22() real ext-real Element of REAL
1 / (r1 + 1) is V22() real ext-real non negative Element of REAL
r2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r2 + 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() V64() V66() Element of NAT
x0 + 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() V64() V66() Element of NAT
1 / (x0 + 1) is V22() real ext-real non negative Element of REAL
1 / (r2 + 1) is V22() real ext-real non negative Element of REAL
r . x0 is V22() real ext-real Element of REAL
(r . x0) - a is V22() real ext-real Element of REAL
abs ((r . x0) - a) is V22() real ext-real Element of REAL
lim r is V22() real ext-real Element of REAL
lim (b /* r) 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() V66() Element of NAT
(b /* r) . s is V22() real ext-real Element of REAL
((b /* r) . s) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* r) . s) - (b . a)) is V22() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
r is V22() real ext-real set
s is V22() real ext-real set
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r2 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . x0 is V22() real ext-real Element of REAL
(u . x0) - a is V22() real ext-real Element of REAL
abs ((u . x0) - a) is V22() real ext-real Element of REAL
b . (u . x0) is V22() real ext-real Element of REAL
(b . (u . x0)) - (b . a) is V22() real ext-real Element of REAL
abs ((b . (u . x0)) - (b . a)) is V22() real ext-real Element of REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* u) . x0 is V22() real ext-real Element of REAL
((b /* u) . x0) - (b . a) is V22() real ext-real Element of REAL
abs (((b /* u) . x0) - (b . a)) is V22() real ext-real Element of REAL
lim (b /* u) is V22() real ext-real Element of REAL
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom a is V45() V46() V47() Element of bool REAL
b is V22() real ext-real set
a . b is V22() real ext-real Element of REAL
u is V45() V46() V47() open Neighbourhood of a . b
r is V22() real ext-real set
(a . b) - r is V22() real ext-real Element of REAL
(a . b) + r is V22() real ext-real Element of REAL
].((a . b) - r),((a . b) + r).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
s is V22() real ext-real set
b - s is V22() real ext-real set
b + s is V22() real ext-real set
].(b - s),(b + s).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
r1 is V45() V46() V47() open Neighbourhood of b
r2 is V22() real ext-real set
a . r2 is V22() real ext-real Element of REAL
r2 - b is V22() real ext-real set
abs (r2 - b) is V22() real ext-real Element of REAL
(a . r2) - (a . b) is V22() real ext-real Element of REAL
abs ((a . r2) - (a . b)) is V22() real ext-real Element of REAL
u is V22() real ext-real set
(a . b) - u is V22() real ext-real Element of REAL
(a . b) + u is V22() real ext-real Element of REAL
].((a . b) - u),((a . b) + u).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
r is V45() V46() V47() open Neighbourhood of a . b
s is V45() V46() V47() open Neighbourhood of b
r1 is V22() real ext-real set
b - r1 is V22() real ext-real set
b + r1 is V22() real ext-real set
].(b - r1),(b + r1).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
r2 is V22() real ext-real set
x0 is V22() real ext-real set
x0 - b is V22() real ext-real set
abs (x0 - b) is V22() real ext-real Element of REAL
a . x0 is V22() real ext-real Element of REAL
(a . x0) - (a . b) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . b)) is V22() real ext-real Element of REAL
x0 is V22() real ext-real set
x0 - b is V22() real ext-real set
abs (x0 - b) is V22() real ext-real Element of REAL
a . x0 is V22() real ext-real Element of REAL
(a . x0) - (a . b) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . b)) is V22() real ext-real Element of REAL
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b is V22() real ext-real set
a . b is V22() real ext-real Element of REAL
u is V45() V46() V47() open Neighbourhood of a . b
dom a is V45() V46() V47() Element of bool REAL
r is V45() V46() V47() open Neighbourhood of b
a .: r is V45() V46() V47() Element of bool REAL
s is V22() real ext-real set
r1 is V22() real ext-real Element of REAL
a . r1 is V22() real ext-real Element of REAL
u is V45() V46() V47() open Neighbourhood of a . b
r is V45() V46() V47() open Neighbourhood of b
a .: r is V45() V46() V47() Element of bool REAL
r1 is V22() real ext-real set
dom a is V45() V46() V47() Element of bool REAL
s is V45() V46() V47() open Neighbourhood of b
a . r1 is V22() real ext-real Element of REAL
a .: s is V45() V46() V47() Element of bool REAL
a is V22() real ext-real set
{a} is non empty trivial V45() V46() V47() Element of bool REAL
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
u is V45() V46() V47() open Neighbourhood of a
(dom b) /\ u is V45() V46() V47() Element of bool REAL
b . a is V22() real ext-real Element of REAL
r is V45() V46() V47() open Neighbourhood of b . a
s is V45() V46() V47() open Neighbourhood of a
b .: s is V45() V46() V47() Element of bool REAL
Im (b,a) is V45() V46() V47() set
{a} is non empty trivial V45() V46() V47() set
b .: {a} is V45() V46() V47() set
{(b . a)} is non empty trivial V45() V46() V47() Element of bool REAL
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom u is V45() V46() V47() Element of bool REAL
(dom b) /\ (dom u) is V45() V46() V47() Element of bool REAL
b + u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b - u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- u is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
- 1 is V22() real ext-real non positive set
(- 1) (#) u is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
b + (- u) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
b (#) u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
dom (b + u) is V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
u /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* r) + (u /* r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b + u) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b . a is V22() real ext-real Element of REAL
lim (b /* r) is V22() real ext-real Element of REAL
u . a is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(b + u) . a is V22() real ext-real Element of REAL
(b . a) + (u . a) is V22() real ext-real Element of REAL
lim ((b /* r) + (u /* r)) is V22() real ext-real Element of REAL
lim ((b + u) /* r) is V22() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
dom (b - u) is V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
u /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* r) - (u /* r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
- (u /* r) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (u /* r) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(b /* r) + (- (u /* r)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(b - u) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* r) is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(b - u) . a is V22() real ext-real Element of REAL
(b . a) - (u . a) is V22() real ext-real Element of REAL
lim ((b /* r) - (u /* r)) is V22() real ext-real Element of REAL
lim ((b - u) /* r) is V22() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
dom (b (#) u) is V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
(b (#) u) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b (#) u) . a is V22() real ext-real Element of REAL
lim ((b (#) u) /* r) is V22() real ext-real Element of REAL
u /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* r) (#) (u /* r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* r) is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(b . a) * (u . a) is V22() real ext-real Element of REAL
lim ((b /* r) (#) (u /* r)) is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is V22() real ext-real set
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom u is V45() V46() V47() Element of bool REAL
b (#) u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (b (#) u) is V45() V46() V47() Element of bool REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
(b (#) u) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b (#) u) . a is V22() real ext-real Element of REAL
lim ((b (#) u) /* r) is V22() real ext-real Element of REAL
u . a is V22() real ext-real Element of REAL
u /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (u /* r) is V22() real ext-real Element of REAL
b (#) (u /* r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b * (u . a) is V22() real ext-real Element of REAL
lim (b (#) (u /* r)) is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
abs b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of bool [:REAL,REAL:]
- b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- 1 is V22() real ext-real non positive set
(- 1) (#) b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
dom (abs b) is V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
b . a is V22() real ext-real Element of REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* u) is V22() real ext-real Element of REAL
abs (b /* u) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued bounded_below Element of bool [:NAT,REAL:]
(abs b) /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(abs b) . a is V22() real ext-real Element of REAL
abs (b . a) is V22() real ext-real Element of REAL
lim (abs (b /* u)) is V22() real ext-real Element of REAL
lim ((abs b) /* u) is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b . a is V22() real ext-real Element of REAL
b ^ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
{0} is functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() Element of bool REAL
b " {0} is V45() V46() V47() Element of bool REAL
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
dom (b ^) is V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
(b ^) /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b ^) . a is V22() real ext-real Element of REAL
lim ((b ^) /* u) is V22() real ext-real Element of REAL
dom b is V45() V46() V47() Element of bool REAL
(dom b) \ (b " {0}) is V45() V46() V47() Element of bool REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim (b /* u) is V22() real ext-real Element of REAL
(b /* u) " is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b . a) " is V22() real ext-real Element of REAL
lim ((b /* u) ") is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u . a is V22() real ext-real Element of REAL
b / u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
{0} is functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() Element of bool REAL
u " {0} is V45() V46() V47() Element of bool REAL
dom u is V45() V46() V47() Element of bool REAL
(dom u) \ (u " {0}) is V45() V46() V47() Element of bool REAL
u ^ is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (u ^) is V45() V46() V47() Element of bool REAL
(dom (u ^)) /\ (dom b) is V45() V46() V47() Element of bool REAL
b (#) (u ^) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is V22() real ext-real set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b * u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (b * u) is V45() V46() V47() Element of bool REAL
u . a is V22() real ext-real Element of REAL
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
(b * u) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b * u) . a is V22() real ext-real Element of REAL
lim ((b * u) /* r) is V22() real ext-real Element of REAL
dom u is V45() V46() V47() Element of bool REAL
s is set
u /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng (u /* r) is non empty V45() V46() V47() Element of bool REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
(u /* r) . r1 is V22() real ext-real Element of REAL
r . r1 is V22() real ext-real Element of REAL
u . (r . r1) is V22() real ext-real Element of REAL
dom b is V45() V46() V47() Element of bool REAL
s is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
r . s is V22() real ext-real Element of REAL
((b * u) /* r) . s is V22() real ext-real Element of REAL
(b * u) . (r . s) is V22() real ext-real Element of REAL
u . (r . s) is V22() real ext-real Element of REAL
b . (u . (r . s)) is V22() real ext-real Element of REAL
(u /* r) . s is V22() real ext-real Element of REAL
b . ((u /* r) . s) is V22() real ext-real Element of REAL
b /* (u /* r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* (u /* r)) . s is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
b . (u . a) is V22() real ext-real Element of REAL
lim (b /* (u /* r)) is V22() real ext-real Element of REAL
a is set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
dom (b | a) is Element of bool a
bool a is set
(dom b) /\ a is V45() V46() V47() Element of bool REAL
r is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
u . r is V22() real ext-real Element of REAL
(b | a) /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((b | a) /* u) . r is V22() real ext-real Element of REAL
(b | a) . (u . r) is V22() real ext-real Element of REAL
b . (u . r) is V22() real ext-real Element of REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* u) . r is V22() real ext-real Element of REAL
b . (lim u) is V22() real ext-real Element of REAL
(b | a) . (lim u) is V22() real ext-real Element of REAL
lim (b /* u) is V22() real ext-real Element of REAL
u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng u is non empty V45() V46() V47() Element of bool REAL
lim u is V22() real ext-real Element of REAL
b /* u is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b . (lim u) is V22() real ext-real Element of REAL
lim (b /* u) is V22() real ext-real Element of REAL
dom (b | a) is Element of bool a
bool a is set
(dom b) /\ a is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
lim r 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() V66() Element of NAT
r . s is V22() real ext-real Element of REAL
(b | a) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((b | a) /* r) . s is V22() real ext-real Element of REAL
(b | a) . (r . s) is V22() real ext-real Element of REAL
b . (r . s) is V22() real ext-real Element of REAL
b /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(b /* r) . s is V22() real ext-real Element of REAL
(b | a) . (lim r) is V22() real ext-real Element of REAL
b . (lim r) is V22() real ext-real Element of REAL
lim ((b | a) /* r) is V22() real ext-real Element of REAL
(b | a) . u is V22() real ext-real Element of REAL
a is set
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom b is V45() V46() V47() Element of bool REAL
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u is V22() real ext-real set
b . u is V22() real ext-real Element of REAL
r is V22() real ext-real set
dom (b | a) is Element of bool a
bool a is set
(b | a) . u is V22() real ext-real Element of REAL
s is V22() real ext-real set
r1 is V22() real ext-real set
r1 - u is V22() real ext-real set
abs (r1 - u) is V22() real ext-real Element of REAL
b . r1 is V22() real ext-real Element of REAL
(b . r1) - (b . u) is V22() real ext-real Element of REAL
abs ((b . r1) - (b . u)) is V22() real ext-real Element of REAL
(dom b) /\ a is V45() V46() V47() Element of bool REAL
(b | a) . r1 is V22() real ext-real Element of REAL
((b | a) . r1) - (b . u) is V22() real ext-real Element of REAL
abs (((b | a) . r1) - (b . u)) is V22() real ext-real Element of REAL
((b | a) . r1) - ((b | a) . u) is V22() real ext-real Element of REAL
abs (((b | a) . r1) - ((b | a) . u)) is V22() real ext-real Element of REAL
u is V22() real ext-real set
dom (b | a) is Element of bool a
bool a is set
(b | a) . u is V22() real ext-real Element of REAL
r is V22() real ext-real set
b . u is V22() real ext-real Element of REAL
s is V22() real ext-real set
r1 is V22() real ext-real set
r1 - u is V22() real ext-real set
abs (r1 - u) is V22() real ext-real Element of REAL
(b | a) . r1 is V22() real ext-real Element of REAL
((b | a) . r1) - ((b | a) . u) is V22() real ext-real Element of REAL
abs (((b | a) . r1) - ((b | a) . u)) is V22() real ext-real Element of REAL
((b | a) . r1) - (b . u) is V22() real ext-real Element of REAL
abs (((b | a) . r1) - (b . u)) is V22() real ext-real Element of REAL
b . r1 is V22() real ext-real Element of REAL
(b . r1) - (b . u) is V22() real ext-real Element of REAL
abs ((b . r1) - (b . u)) is V22() real ext-real Element of REAL
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u is V22() real ext-real set
dom a is V45() V46() V47() Element of bool REAL
r is V22() real ext-real set
b is V22() real ext-real set
s is V22() real ext-real set
r1 is V22() real ext-real set
r1 - u is V22() real ext-real set
abs (r1 - u) is V22() real ext-real Element of REAL
a . r1 is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
(a . r1) - (a . u) is V22() real ext-real Element of REAL
abs ((a . r1) - (a . u)) is V22() real ext-real Element of REAL
a | (dom a) is Relation-like REAL -defined dom a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
the Relation-like REAL -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued non-decreasing non-increasing bounded_above bounded_below monotone bounded () Element of bool [:REAL,REAL:] is Relation-like REAL -defined REAL -valued Function-like constant complex-valued ext-real-valued real-valued non-decreasing non-increasing bounded_above bounded_below monotone bounded () Element of bool [:REAL,REAL:]
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
b is set
a | b is Relation-like REAL -defined b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (a | b) is Element of bool b
bool b is set
u is V22() real ext-real set
dom a is V45() V46() V47() Element of bool REAL
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is set
b | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b | a) | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u is set
r | u is Relation-like REAL -defined u -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(r | u) | u is Relation-like REAL -defined u -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is set
b is set
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u | b is Relation-like REAL -defined b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | a) | b is Relation-like REAL -defined b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b is trivial set
a | b is Relation-like REAL -defined b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (a | b) is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
{u} is non empty trivial V45() V46() V47() Element of bool REAL
r is V22() real ext-real set
dom (a | b) is Element of bool b
bool b is set
s is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng s is non empty V45() V46() V47() Element of bool REAL
lim s is V22() real ext-real Element of REAL
(a | b) /* s is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(a | b) . r is V22() real ext-real Element of REAL
lim ((a | b) /* s) is V22() real ext-real Element of REAL
dom a is V45() V46() V47() Element of bool REAL
(dom a) /\ {u} is V45() V46() V47() Element of bool REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
s . r1 is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
r2 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty trivial epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() real ext-real non positive non negative V33() V34() complex-valued ext-real-valued real-valued natural-valued increasing decreasing non-decreasing non-increasing V45() V46() V47() V48() V49() V50() V51() bounded_above bounded_below V66() V69() bounded Element of NAT
x0 is epsilon-transitive epsilon-connected ordinal natural V22() real ext-real non negative V33() V34() V45() V46() V47() V48() V49() V50() V66() Element of NAT
a | {u} is Relation-like REAL -defined {u} -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a | {u}) /* s is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
((a | {u}) /* s) . x0 is V22() real ext-real Element of REAL
(a | {u}) . r is V22() real ext-real Element of REAL
(((a | {u}) /* s) . x0) - ((a | {u}) . r) is V22() real ext-real Element of REAL
abs ((((a | {u}) /* s) . x0) - ((a | {u}) . r)) is V22() real ext-real Element of REAL
s . x0 is V22() real ext-real Element of REAL
(a | {u}) . (s . x0) is V22() real ext-real Element of REAL
(a | {u}) . u is V22() real ext-real Element of REAL
((a | {u}) . (s . x0)) - ((a | {u}) . u) is V22() real ext-real Element of REAL
abs (((a | {u}) . (s . x0)) - ((a | {u}) . u)) is V22() real ext-real Element of REAL
((a | {u}) . u) - ((a | {u}) . u) is V22() real ext-real Element of REAL
abs (((a | {u}) . u) - ((a | {u}) . u)) is V22() real ext-real Element of REAL
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is V22() real ext-real set
{a} is non empty trivial V45() V46() V47() Element of bool REAL
b | {a} is Relation-like REAL -defined {a} -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
a + b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom (a + b) is V45() V46() V47() Element of bool REAL
dom a is V45() V46() V47() Element of bool REAL
dom b is V45() V46() V47() Element of bool REAL
(dom a) /\ (dom b) is V45() V46() V47() Element of bool REAL
a | (dom (a + b)) is Relation-like REAL -defined dom (a + b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
b | (dom (a + b)) is Relation-like REAL -defined dom (a + b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
rng r is non empty V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
a /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
b /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
(a /* r) + (b /* r) is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
a . (lim r) is V22() real ext-real Element of REAL
lim (a /* r) is V22() real ext-real Element of REAL
b . (lim r) is V22() real ext-real Element of REAL
lim (b /* r) is V22() real ext-real Element of REAL
(a + b) . (lim r) is V22() real ext-real Element of REAL
(lim (a /* r)) + (lim (b /* r)) is V22() real ext-real Element of REAL
lim ((a /* r) + (b /* r)) is V22() real ext-real Element of REAL
(a + b) /* r is Relation-like NAT -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,REAL:]
lim ((a + b) /* r) is