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 V22() real ext-real Element of REAL
(a + 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 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:]
- b 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) (#) b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
a + (- b) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
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:]
- (b /* r) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(- 1) (#) (b /* r) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
(a /* r) + (- (b /* r)) is Relation-like NAT -defined Function-like total complex-valued ext-real-valued real-valued set
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 V22() real ext-real Element of REAL
(a - 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 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 V22() real ext-real Element of REAL
(a (#) 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 REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,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 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
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:]
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) | 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 - 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) (#) 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) | 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 (#) u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b (#) 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
lim r 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:]
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) (#) (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 . (lim r) is V22() real ext-real Element of REAL
lim (b /* r) is V22() real ext-real Element of REAL
u . (lim r) is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(b (#) u) . (lim r) is V22() real ext-real Element of REAL
(lim (b /* r)) * (lim (u /* r)) is V22() real ext-real Element of REAL
lim ((b /* r) (#) (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:]
lim ((b (#) u) /* r) is V22() real ext-real Element of 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 /* 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 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 . (lim r) is V22() real ext-real Element of REAL
lim (b /* r) is V22() real ext-real Element of REAL
u . (lim r) is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(b + u) . (lim r) is V22() real ext-real Element of REAL
(lim (b /* r)) + (lim (u /* r)) is V22() real ext-real Element of REAL
lim ((b /* r) + (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:]
lim ((b + u) /* r) is V22() real ext-real Element of 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 /* 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 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 . (lim r) is V22() real ext-real Element of REAL
lim (b /* r) is V22() real ext-real Element of REAL
u . (lim r) is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(b - u) . (lim r) is V22() real ext-real Element of REAL
(lim (b /* r)) - (lim (u /* r)) is V22() real ext-real Element of REAL
lim ((b /* r) - (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:]
lim ((b - u) /* r) is V22() real ext-real Element of REAL
dom (b (#) u) is V45() V46() V47() Element of bool REAL
a is set
b is set
a /\ 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:]
dom u is V45() V46() V47() Element of bool 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 REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom r is V45() V46() V47() Element of bool REAL
r | 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 + r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u + r) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u - r 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 REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) r is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
u + (- r) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(u - r) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u (#) r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u (#) r) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(dom u) /\ (dom r) is V45() V46() V47() Element of bool REAL
u | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | (a /\ b) is Relation-like REAL -defined a /\ 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:]
b is V22() real ext-real set
b (#) 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
dom (b (#) a) is V45() V46() V47() Element of bool 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:]
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 (#) (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:]
a . (lim r) is V22() real ext-real Element of REAL
lim (a /* r) is V22() real ext-real Element of REAL
(b (#) a) . (lim r) is V22() real ext-real Element of REAL
b * (lim (a /* r)) is V22() real ext-real Element of REAL
lim (b (#) (a /* r)) 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:]
lim ((b (#) a) /* r) is V22() real ext-real Element of REAL
(b (#) 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:]
r 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 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
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:]
a (#) u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a (#) 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:]
dom (a (#) 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
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:]
a (#) (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 . (lim r) is V22() real ext-real Element of REAL
lim (u /* r) is V22() real ext-real Element of REAL
(a (#) u) . (lim r) is V22() real ext-real Element of REAL
a * (lim (u /* r)) is V22() real ext-real Element of REAL
lim (a (#) (u /* r)) is V22() real ext-real Element of REAL
(a (#) 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 ((a (#) 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:]
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:]
(abs b) | a is Relation-like REAL -defined a -defined 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) (#) b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued 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:]
u is V22() real ext-real set
dom ((abs b) | a) is V45() V46() V47() Element of bool REAL
dom ((abs b) | a) is Element of bool a
bool a is set
dom (abs b) is V45() V46() V47() Element of bool REAL
dom (b | a) is Element of bool 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:]
rng r is non empty V45() V46() V47() Element of bool REAL
lim r is V22() real ext-real Element of REAL
((abs 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:]
((abs b) | a) . u is V22() real ext-real Element of REAL
lim (((abs b) | a) /* r) is V22() real ext-real Element of REAL
(dom (abs b)) /\ a is V45() V46() V47() Element of bool REAL
(dom b) /\ a 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 | 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:]
abs ((b | a) /* r) 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 | a) /* r)) . s is V22() real ext-real Element of REAL
((b | a) /* r) . s is V22() real ext-real Element of REAL
abs (((b | a) /* r) . s) is V22() real ext-real Element of REAL
(b | a) . (r . s) is V22() real ext-real Element of REAL
abs ((b | a) . (r . s)) is V22() real ext-real Element of REAL
b . (r . s) is V22() real ext-real Element of REAL
abs (b . (r . s)) is V22() real ext-real Element of REAL
(abs b) . (r . s) is V22() real ext-real Element of REAL
((abs b) | a) . (r . s) is V22() real ext-real Element of REAL
(((abs b) | a) /* r) . s is V22() real ext-real Element of REAL
(b | a) . u is V22() real ext-real Element of REAL
abs ((b | a) . u) is V22() real ext-real Element of REAL
b . u is V22() real ext-real Element of REAL
abs (b . u) is V22() real ext-real Element of REAL
(abs b) . u is V22() real ext-real Element of REAL
lim ((b | a) /* r) is V22() real ext-real Element of REAL
{0} is functional non empty trivial V45() V46() V47() V48() V49() V50() V64() V66() Element of bool 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:]
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 " {0} is 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:]
(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:]
dom (b ^) is V45() V46() V47() Element of bool REAL
dom b is V45() V46() V47() Element of bool REAL
(dom b) \ {} is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
dom ((b ^) | a) is V45() V46() V47() Element of bool REAL
dom ((b ^) | a) is Element of bool a
bool a is set
dom (b | a) is Element of bool a
b . u 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
(dom (b ^)) /\ a is V45() V46() V47() Element of bool 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:]
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
(dom b) /\ a is V45() V46() V47() Element of bool REAL
b . (r . s) is V22() real ext-real Element of 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
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 . s) is V22() real ext-real Element of REAL
(b . (r . s)) " is V22() real ext-real Element of 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 | a) /* r) . s is V22() real ext-real Element of REAL
(((b | a) /* 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) . u is V22() real ext-real Element of REAL
lim ((b | a) /* 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
(b . u) " is V22() real ext-real Element of REAL
(b ^) . u 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:]
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) " {0} is 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:]
(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:]
(b | a) ^ is Relation-like 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:]
((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:]
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:]
b " {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 b) /\ (dom u) is V45() V46() V47() Element of bool 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 REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u / 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 ^ 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
(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 (#) (b ^) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u (#) (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:]
b * 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 (b * a) is V45() V46() V47() Element of bool REAL
a . u is V22() real ext-real Element of REAL
dom b is V45() V46() V47() Element of bool REAL
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:]
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:]
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 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 | (b .: a) is Relation-like REAL -defined b .: 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 REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u * 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 | (b .: a)) * (b | a) 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 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 V45() V46() V47() Element of bool REAL
a /\ (u " b) is V45() V46() V47() Element of bool REAL
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | 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:]
r * u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(r * u) | (a /\ (u " b)) is Relation-like REAL -defined a /\ (u " b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(r | b) * (u | 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:]
a | REAL is Relation-like REAL -defined 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
(a . b) + 0 is V22() real ext-real Element of REAL
b + 0 is V22() real ext-real set
a . (b + 0) is V22() real ext-real Element of REAL
a . 0 is V22() real ext-real Element of REAL
(a . b) + (a . 0) is V22() real ext-real Element of REAL
u is V22() real ext-real set
- u is V22() real ext-real set
u + (- u) is V22() real ext-real set
a . (u + (- u)) is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
a . (- u) is V22() real ext-real Element of REAL
(a . u) + (a . (- u)) is V22() real ext-real Element of REAL
- (a . u) is V22() real ext-real Element of REAL
u is V22() real ext-real set
r is V22() real ext-real set
u - r is V22() real ext-real set
a . (u - r) is V22() real ext-real Element of REAL
- r is V22() real ext-real set
u + (- r) is V22() real ext-real set
a . (u + (- r)) is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
a . (- r) is V22() real ext-real Element of REAL
(a . u) + (a . (- r)) is V22() real ext-real Element of REAL
a . r is V22() real ext-real Element of REAL
- (a . r) is V22() real ext-real Element of REAL
(a . u) + (- (a . r)) is V22() real ext-real Element of REAL
(a . u) - (a . r) is V22() real ext-real Element of REAL
u is V22() real ext-real set
r is V22() real ext-real set
u - b is V22() real ext-real set
r1 is V22() real ext-real set
r2 is V22() real ext-real set
x0 is V22() real ext-real set
x0 - u is V22() real ext-real set
abs (x0 - u) is V22() real ext-real Element of REAL
x0 - (u - b) is V22() real ext-real set
(x0 - (u - b)) - b is V22() real ext-real set
abs ((x0 - (u - b)) - b) is V22() real ext-real Element of REAL
(u - b) + b is V22() real ext-real set
a . x0 is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
(a . x0) - (a . u) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . u)) is V22() real ext-real Element of REAL
a . (u - b) is V22() real ext-real Element of REAL
(a . (u - b)) + (a . b) is V22() real ext-real Element of REAL
(a . x0) - ((a . (u - b)) + (a . b)) is V22() real ext-real Element of REAL
abs ((a . x0) - ((a . (u - b)) + (a . b))) is V22() real ext-real Element of REAL
(a . x0) - (a . (u - b)) is V22() real ext-real Element of REAL
((a . x0) - (a . (u - b))) - (a . b) is V22() real ext-real Element of REAL
abs (((a . x0) - (a . (u - b))) - (a . b)) is V22() real ext-real Element of REAL
a . (x0 - (u - b)) is V22() real ext-real Element of REAL
(a . (x0 - (u - b))) - (a . b) is V22() real ext-real Element of REAL
abs ((a . (x0 - (u - b))) - (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:]
dom a is V45() V46() V47() Element of bool 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:]
rng a is V45() V46() V47() Element of bool REAL
b 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 b is non empty V45() V46() V47() Element of bool REAL
u 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 is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
a . r 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:]
r is set
rng u is non empty 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
u . s 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:]
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
u . s is V22() real ext-real Element of REAL
a . (u . s) is V22() real ext-real Element of REAL
b . s is V22() real ext-real Element of REAL
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:]
(a /* u) . s 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:]
dom (a | (dom a)) is V45() V46() V47() Element of bool REAL
rng r is non empty V45() V46() V47() Element of bool REAL
a . (lim r) is V22() real ext-real Element of REAL
lim (a /* r) is V22() real ext-real Element of REAL
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:]
lim s is V22() real ext-real Element of REAL
a is 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
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 is V45() V46() V47() Element of bool 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:]
dom (b | a) is V45() V46() V47() Element of bool a
bool a is set
(dom b) /\ a is V45() V46() V47() Element of bool REAL
rng (b | a) is V45() V46() V47() Element of bool 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
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:]
rng a is V45() V46() V47() Element of bool REAL
upper_bound (rng a) is V22() real ext-real Element of REAL
lower_bound (rng a) is V22() real ext-real Element of REAL
b is V22() real ext-real Element of REAL
a . b is V22() real ext-real Element of REAL
u is V22() real ext-real Element of REAL
a . 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 V45() V46() V47() Element of bool REAL
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 .: b is V45() V46() V47() Element of bool REAL
upper_bound (a .: b) is V22() real ext-real Element of REAL
lower_bound (a .: b) is V22() real ext-real Element of REAL
dom (a | b) is V45() V46() V47() Element of bool b
bool b is set
(dom a) /\ b is V45() V46() V47() Element of bool REAL
(a | b) | 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:]
rng (a | b) is V45() V46() V47() Element of bool REAL
upper_bound (rng (a | b)) is V22() real ext-real Element of REAL
lower_bound (rng (a | b)) is V22() real ext-real Element of REAL
u is V22() real ext-real set
r is V22() real ext-real set
(a | b) . u is V22() real ext-real Element of REAL
(a | b) . r is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
a . 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:]
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:]
dom (b | a) is Element of bool a
bool a is set
u is V22() real ext-real set
r is V22() real ext-real set
b . r is V22() real ext-real Element of REAL
s is V22() real ext-real set
b . s is V22() real ext-real Element of REAL
(b . r) - (b . s) is V22() real ext-real Element of REAL
abs ((b . r) - (b . s)) is V22() real ext-real Element of REAL
r - s is V22() real ext-real set
abs (r - s) is V22() real ext-real Element of REAL
u * (abs (r - s)) is V22() real ext-real Element of REAL
(b | a) . r is V22() real ext-real Element of REAL
(b | a) . s is V22() real ext-real Element of REAL
u is V22() real ext-real set
dom (b | a) is V45() V46() V47() Element of bool REAL
r is V22() real ext-real set
(b | a) . r is V22() real ext-real Element of REAL
s is V22() real ext-real set
(b | a) . s is V22() real ext-real Element of REAL
((b | a) . r) - ((b | a) . s) is V22() real ext-real Element of REAL
abs (((b | a) . r) - ((b | a) . s)) is V22() real ext-real Element of REAL
r - s is V22() real ext-real set
abs (r - s) is V22() real ext-real Element of REAL
u * (abs (r - s)) is V22() real ext-real Element of REAL
b . r is V22() real ext-real Element of REAL
b . s 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
u is V22() real ext-real set
a . b is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
(a . b) - (a . u) is V22() real ext-real Element of REAL
abs ((a . b) - (a . u)) is V22() real ext-real Element of REAL
b - u is V22() real ext-real set
abs (b - u) is V22() real ext-real Element of REAL
1 * (abs (b - u)) is V22() real ext-real Element of REAL
the Relation-like non-empty empty-yielding REAL -defined REAL -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() monotone bounded () () Element of bool [:REAL,REAL:] is Relation-like non-empty empty-yielding REAL -defined REAL -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() 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 is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
r is V22() real ext-real set
dom (a | b) is Element of bool b
bool b is set
s is V22() real ext-real set
a . r is V22() real ext-real Element of REAL
a . s is V22() real ext-real Element of REAL
(a . r) - (a . s) is V22() real ext-real Element of REAL
abs ((a . r) - (a . s)) is V22() real ext-real Element of REAL
r - s is V22() real ext-real set
abs (r - s) is V22() real ext-real Element of REAL
u * (abs (r - s)) 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:]
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:]
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 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) /\ (dom b)) is Relation-like REAL -defined (dom a) /\ (dom b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
dom (a | ((dom a) /\ (dom b))) is V45() V46() V47() Element of bool ((dom a) /\ (dom b))
bool ((dom a) /\ (dom b)) is set
s is V22() real ext-real set
b | ((dom a) /\ (dom b)) is Relation-like REAL -defined (dom a) /\ (dom b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
dom (b | ((dom a) /\ (dom b))) is V45() V46() V47() Element of bool ((dom a) /\ (dom b))
r1 is V22() real ext-real set
s + r1 is V22() real ext-real set
r2 is V22() real ext-real set
x0 is V22() real ext-real set
dom (a + b) is V45() V46() V47() Element of bool REAL
N1 is V22() real ext-real set
(a + b) . x0 is V22() real ext-real Element of REAL
(a + b) . N1 is V22() real ext-real Element of REAL
((a + b) . x0) - ((a + b) . N1) is V22() real ext-real Element of REAL
abs (((a + b) . x0) - ((a + b) . N1)) is V22() real ext-real Element of REAL
a . x0 is V22() real ext-real Element of REAL
b . x0 is V22() real ext-real Element of REAL
(a . x0) + (b . x0) is V22() real ext-real Element of REAL
((a . x0) + (b . x0)) - ((a + b) . N1) is V22() real ext-real Element of REAL
abs (((a . x0) + (b . x0)) - ((a + b) . N1)) is V22() real ext-real Element of REAL
a . N1 is V22() real ext-real Element of REAL
b . N1 is V22() real ext-real Element of REAL
(a . N1) + (b . N1) is V22() real ext-real Element of REAL
((a . x0) + (b . x0)) - ((a . N1) + (b . N1)) is V22() real ext-real Element of REAL
abs (((a . x0) + (b . x0)) - ((a . N1) + (b . N1))) is V22() real ext-real Element of REAL
(a . x0) - (a . N1) is V22() real ext-real Element of REAL
(b . x0) - (b . N1) is V22() real ext-real Element of REAL
((a . x0) - (a . N1)) + ((b . x0) - (b . N1)) is V22() real ext-real Element of REAL
abs (((a . x0) - (a . N1)) + ((b . x0) - (b . N1))) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . N1)) is V22() real ext-real Element of REAL
abs ((b . x0) - (b . N1)) is V22() real ext-real Element of REAL
(abs ((a . x0) - (a . N1))) + (abs ((b . x0) - (b . N1))) is V22() real ext-real Element of REAL
(dom b) /\ ((dom a) /\ (dom b)) is V45() V46() V47() Element of bool REAL
(dom b) /\ (dom b) is V45() V46() V47() Element of bool REAL
((dom b) /\ (dom b)) /\ (dom a) is V45() V46() V47() Element of bool REAL
x0 - N1 is V22() real ext-real set
abs (x0 - N1) is V22() real ext-real Element of REAL
r1 * (abs (x0 - N1)) is V22() real ext-real Element of REAL
(dom a) /\ ((dom a) /\ (dom b)) is V45() V46() V47() Element of bool REAL
(dom a) /\ (dom a) is V45() V46() V47() Element of bool REAL
((dom a) /\ (dom a)) /\ (dom b) is V45() V46() V47() Element of bool REAL
s * (abs (x0 - N1)) is V22() real ext-real Element of REAL
(s * (abs (x0 - N1))) + (r1 * (abs (x0 - N1))) is V22() real ext-real Element of REAL
r2 * (abs (x0 - N1)) is V22() real ext-real Element of REAL
r2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x0 is V22() real ext-real set
a - b 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 Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) b is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
a + (- b) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
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) /\ (dom b)) is Relation-like REAL -defined (dom a) /\ (dom b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
dom (a | ((dom a) /\ (dom b))) is V45() V46() V47() Element of bool ((dom a) /\ (dom b))
bool ((dom a) /\ (dom b)) is set
s is V22() real ext-real set
b | ((dom a) /\ (dom b)) is Relation-like REAL -defined (dom a) /\ (dom b) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
dom (b | ((dom a) /\ (dom b))) is V45() V46() V47() Element of bool ((dom a) /\ (dom b))
r1 is V22() real ext-real set
s + r1 is V22() real ext-real set
r2 is V22() real ext-real set
x0 is V22() real ext-real set
dom (a - b) is V45() V46() V47() Element of bool REAL
N1 is V22() real ext-real set
(a - b) . x0 is V22() real ext-real Element of REAL
(a - b) . N1 is V22() real ext-real Element of REAL
((a - b) . x0) - ((a - b) . N1) is V22() real ext-real Element of REAL
abs (((a - b) . x0) - ((a - b) . N1)) is V22() real ext-real Element of REAL
a . x0 is V22() real ext-real Element of REAL
b . x0 is V22() real ext-real Element of REAL
(a . x0) - (b . x0) is V22() real ext-real Element of REAL
((a . x0) - (b . x0)) - ((a - b) . N1) is V22() real ext-real Element of REAL
abs (((a . x0) - (b . x0)) - ((a - b) . N1)) is V22() real ext-real Element of REAL
a . N1 is V22() real ext-real Element of REAL
b . N1 is V22() real ext-real Element of REAL
(a . N1) - (b . N1) is V22() real ext-real Element of REAL
((a . x0) - (b . x0)) - ((a . N1) - (b . N1)) is V22() real ext-real Element of REAL
abs (((a . x0) - (b . x0)) - ((a . N1) - (b . N1))) is V22() real ext-real Element of REAL
(a . x0) - (a . N1) is V22() real ext-real Element of REAL
(b . x0) - (b . N1) is V22() real ext-real Element of REAL
((a . x0) - (a . N1)) - ((b . x0) - (b . N1)) is V22() real ext-real Element of REAL
abs (((a . x0) - (a . N1)) - ((b . x0) - (b . N1))) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . N1)) is V22() real ext-real Element of REAL
abs ((b . x0) - (b . N1)) is V22() real ext-real Element of REAL
(abs ((a . x0) - (a . N1))) + (abs ((b . x0) - (b . N1))) is V22() real ext-real Element of REAL
(dom b) /\ ((dom a) /\ (dom b)) is V45() V46() V47() Element of bool REAL
(dom b) /\ (dom b) is V45() V46() V47() Element of bool REAL
((dom b) /\ (dom b)) /\ (dom a) is V45() V46() V47() Element of bool REAL
x0 - N1 is V22() real ext-real set
abs (x0 - N1) is V22() real ext-real Element of REAL
r1 * (abs (x0 - N1)) is V22() real ext-real Element of REAL
(dom a) /\ ((dom a) /\ (dom b)) is V45() V46() V47() Element of bool REAL
(dom a) /\ (dom a) is V45() V46() V47() Element of bool REAL
((dom a) /\ (dom a)) /\ (dom b) is V45() V46() V47() Element of bool REAL
s * (abs (x0 - N1)) is V22() real ext-real Element of REAL
(s * (abs (x0 - N1))) + (r1 * (abs (x0 - N1))) is V22() real ext-real Element of REAL
r2 * (abs (x0 - N1)) is V22() real ext-real Element of REAL
r2 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
x0 is V22() real ext-real set
a is set
b is set
a /\ 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:]
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | 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 + r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u + r) | (a /\ b) is Relation-like REAL -defined a /\ 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 a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | a) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(r | b) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | (a /\ b)) + (r | (a /\ 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 is set
a /\ 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:]
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | 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 - r 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 REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) r is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
u + (- r) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(u - r) | (a /\ b) is Relation-like REAL -defined a /\ 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 a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | a) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(r | b) | (a /\ b) is Relation-like REAL -defined a /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | (a /\ b)) - (r | (a /\ b)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
- (r | (a /\ b)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(- 1) (#) (r | (a /\ b)) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
(u | (a /\ b)) + (- (r | (a /\ b))) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded () Element of bool [:REAL,REAL:]
b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded () Element of bool [:REAL,REAL:]
a (#) b is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_above bounded_below bounded Element of bool [:REAL,REAL:]
dom a is V45() V46() V47() Element of bool REAL
dom b is V45() V46() V47() Element of bool REAL
s is V22() real ext-real set
r1 is V22() real ext-real set
r2 is V22() real ext-real set
x0 is V22() real ext-real set
N1 is V22() real ext-real set
dom (a (#) b) is V45() V46() V47() Element of bool REAL
(dom a) /\ (dom b) is V45() V46() V47() Element of bool REAL
a . N1 is V22() real ext-real Element of REAL
abs (a . N1) is V22() real ext-real Element of REAL
b . N1 is V22() real ext-real Element of REAL
abs (b . N1) is V22() real ext-real Element of REAL
abs s is V22() real ext-real Element of REAL
abs r1 is V22() real ext-real Element of REAL
(abs s) * r2 is V22() real ext-real Element of REAL
(abs r1) * x0 is V22() real ext-real Element of REAL
((abs s) * r2) + ((abs r1) * x0) is V22() real ext-real Element of REAL
(((abs s) * r2) + ((abs r1) * x0)) + 1 is V22() real ext-real Element of REAL
N1 is V22() real ext-real Element of REAL
N is V22() real ext-real set
N is V22() real ext-real set
a . N is V22() real ext-real Element of REAL
b . N is V22() real ext-real Element of REAL
b . N is V22() real ext-real Element of REAL
(b . N) - (b . N) is V22() real ext-real Element of REAL
(a . N) * ((b . N) - (b . N)) is V22() real ext-real Element of REAL
abs ((a . N) * ((b . N) - (b . N))) is V22() real ext-real Element of REAL
abs (a . N) is V22() real ext-real Element of REAL
abs ((b . N) - (b . N)) is V22() real ext-real Element of REAL
(abs (a . N)) * (abs ((b . N) - (b . N))) is V22() real ext-real Element of REAL
(abs s) * (abs ((b . N) - (b . N))) is V22() real ext-real Element of REAL
N - N is V22() real ext-real set
abs (N - N) is V22() real ext-real Element of REAL
r2 * (abs (N - N)) is V22() real ext-real Element of REAL
(abs s) * (r2 * (abs (N - N))) is V22() real ext-real Element of REAL
((abs s) * r2) * (abs (N - N)) is V22() real ext-real Element of REAL
(((abs s) * r2) + ((abs r1) * x0)) * (abs (N - N)) is V22() real ext-real Element of REAL
((((abs s) * r2) + ((abs r1) * x0)) * (abs (N - N))) + 0 is V22() real ext-real Element of REAL
1 * (abs (N - N)) is V22() real ext-real Element of REAL
((((abs s) * r2) + ((abs r1) * x0)) * (abs (N - N))) + (1 * (abs (N - N))) is V22() real ext-real Element of REAL
(a (#) b) . N is V22() real ext-real Element of REAL
(a (#) b) . N is V22() real ext-real Element of REAL
((a (#) b) . N) - ((a (#) b) . N) is V22() real ext-real Element of REAL
abs (((a (#) b) . N) - ((a (#) b) . N)) is V22() real ext-real Element of REAL
(a . N) * (b . N) is V22() real ext-real Element of REAL
((a . N) * (b . N)) - ((a (#) b) . N) is V22() real ext-real Element of REAL
abs (((a . N) * (b . N)) - ((a (#) b) . N)) is V22() real ext-real Element of REAL
(a . N) * (b . N) is V22() real ext-real Element of REAL
((a . N) * (b . N)) - ((a . N) * (b . N)) is V22() real ext-real Element of REAL
((a . N) * (b . N)) + (((a . N) * (b . N)) - ((a . N) * (b . N))) is V22() real ext-real Element of REAL
a . N is V22() real ext-real Element of REAL
(a . N) * (b . N) is V22() real ext-real Element of REAL
(((a . N) * (b . N)) + (((a . N) * (b . N)) - ((a . N) * (b . N)))) - ((a . N) * (b . N)) is V22() real ext-real Element of REAL
abs ((((a . N) * (b . N)) + (((a . N) * (b . N)) - ((a . N) * (b . N)))) - ((a . N) * (b . N))) is V22() real ext-real Element of REAL
(a . N) - (a . N) is V22() real ext-real Element of REAL
((a . N) - (a . N)) * (b . N) is V22() real ext-real Element of REAL
((a . N) * ((b . N) - (b . N))) + (((a . N) - (a . N)) * (b . N)) is V22() real ext-real Element of REAL
abs (((a . N) * ((b . N) - (b . N))) + (((a . N) - (a . N)) * (b . N))) is V22() real ext-real Element of REAL
abs (((a . N) - (a . N)) * (b . N)) is V22() real ext-real Element of REAL
(abs ((a . N) * ((b . N) - (b . N)))) + (abs (((a . N) - (a . N)) * (b . N))) is V22() real ext-real Element of REAL
abs (b . N) is V22() real ext-real Element of REAL
abs ((a . N) - (a . N)) is V22() real ext-real Element of REAL
(abs (b . N)) * (abs ((a . N) - (a . N))) is V22() real ext-real Element of REAL
(abs r1) * (abs ((a . N) - (a . N))) is V22() real ext-real Element of REAL
x0 * (abs (N - N)) is V22() real ext-real Element of REAL
(abs r1) * (x0 * (abs (N - N))) is V22() real ext-real Element of REAL
((abs r1) * x0) * (abs (N - N)) is V22() real ext-real Element of REAL
(((abs s) * r2) * (abs (N - N))) + (((abs r1) * x0) * (abs (N - N))) is V22() real ext-real Element of REAL
N1 * (abs (N - N)) is V22() real ext-real Element of REAL
N1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
N is V22() real ext-real Element of REAL
a is set
b is set
u is set
a /\ u is set
(a /\ u) /\ b is set
r is set
((a /\ u) /\ b) /\ r is set
s is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
s | 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:]
s | 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:]
r1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r1 | 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:]
r1 | r is Relation-like REAL -defined r -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
s (#) r1 is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(s (#) r1) | (((a /\ u) /\ b) /\ r) is Relation-like REAL -defined ((a /\ u) /\ b) /\ r -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
s | (((a /\ u) /\ b) /\ r) is Relation-like REAL -defined ((a /\ u) /\ b) /\ r -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b /\ r is set
(b /\ r) /\ (a /\ u) is set
s | ((b /\ r) /\ (a /\ u)) is Relation-like REAL -defined (b /\ r) /\ (a /\ u) -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b /\ r) /\ a is set
((b /\ r) /\ a) /\ u is set
s | (((b /\ r) /\ a) /\ u) is Relation-like REAL -defined ((b /\ r) /\ a) /\ u -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(s | u) | ((b /\ r) /\ a) is Relation-like REAL -defined (b /\ r) /\ a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(b /\ r) /\ u is set
((b /\ r) /\ u) /\ a is set
s | (((b /\ r) /\ u) /\ a) is Relation-like REAL -defined ((b /\ r) /\ u) /\ a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(s | a) | ((b /\ r) /\ u) is Relation-like REAL -defined (b /\ r) /\ u -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r1 | (((a /\ u) /\ b) /\ r) is Relation-like REAL -defined ((a /\ u) /\ b) /\ r -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(a /\ u) /\ r is set
((a /\ u) /\ r) /\ b is set
r1 | (((a /\ u) /\ r) /\ b) is Relation-like REAL -defined ((a /\ u) /\ r) /\ b -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u /\ a is set
(u /\ a) /\ r is set
(r1 | b) | ((u /\ a) /\ r) is Relation-like REAL -defined (u /\ a) /\ r -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(s | (((a /\ u) /\ b) /\ r)) (#) (r1 | (((a /\ u) /\ b) /\ r)) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(r1 | r) | ((a /\ u) /\ b) is Relation-like REAL -defined (a /\ u) /\ 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:]
b is V22() real ext-real set
b (#) 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
u is V22() real ext-real set
r is V22() real ext-real set
s is V22() real ext-real set
dom (b (#) a) is V45() V46() V47() Element of bool REAL
r1 is V22() real ext-real set
s - r1 is V22() real ext-real set
abs (s - r1) is V22() real ext-real Element of REAL
(b (#) a) . s is V22() real ext-real Element of REAL
(b (#) a) . r1 is V22() real ext-real Element of REAL
((b (#) a) . s) - ((b (#) a) . r1) is V22() real ext-real Element of REAL
abs (((b (#) a) . s) - ((b (#) a) . r1)) is V22() real ext-real Element of REAL
a . s is V22() real ext-real Element of REAL
b * (a . s) is V22() real ext-real Element of REAL
(b * (a . s)) - ((b (#) a) . r1) is V22() real ext-real Element of REAL
abs ((b * (a . s)) - ((b (#) a) . r1)) is V22() real ext-real Element of REAL
a . r1 is V22() real ext-real Element of REAL
b * (a . r1) is V22() real ext-real Element of REAL
0 - (b * (a . r1)) is V22() real ext-real Element of REAL
abs (0 - (b * (a . r1))) is V22() real ext-real Element of REAL
r * (abs (s - r1)) 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:]
s is V22() real ext-real set
abs b is V22() real ext-real Element of REAL
(abs b) * u is V22() real ext-real Element of REAL
0 * u is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
s is V22() real ext-real set
dom (b (#) a) is V45() V46() V47() Element of bool REAL
r1 is V22() real ext-real set
(b (#) a) . s is V22() real ext-real Element of REAL
(b (#) a) . r1 is V22() real ext-real Element of REAL
((b (#) a) . s) - ((b (#) a) . r1) is V22() real ext-real Element of REAL
abs (((b (#) a) . s) - ((b (#) a) . r1)) is V22() real ext-real Element of REAL
a . s is V22() real ext-real Element of REAL
b * (a . s) is V22() real ext-real Element of REAL
(b * (a . s)) - ((b (#) a) . r1) is V22() real ext-real Element of REAL
abs ((b * (a . s)) - ((b (#) a) . r1)) is V22() real ext-real Element of REAL
a . r1 is V22() real ext-real Element of REAL
b * (a . r1) is V22() real ext-real Element of REAL
(b * (a . s)) - (b * (a . r1)) is V22() real ext-real Element of REAL
abs ((b * (a . s)) - (b * (a . r1))) is V22() real ext-real Element of REAL
(a . s) - (a . r1) is V22() real ext-real Element of REAL
b * ((a . s) - (a . r1)) is V22() real ext-real Element of REAL
abs (b * ((a . s) - (a . r1))) is V22() real ext-real Element of REAL
abs ((a . s) - (a . r1)) is V22() real ext-real Element of REAL
(abs b) * (abs ((a . s) - (a . r1))) is V22() real ext-real Element of REAL
s - r1 is V22() real ext-real set
abs (s - r1) is V22() real ext-real Element of REAL
u * (abs (s - r1)) is V22() real ext-real Element of REAL
(abs b) * (u * (abs (s - r1))) is V22() real ext-real Element of REAL
r * (abs (s - r1)) 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:]
s is V22() real ext-real Element of REAL
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:]
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) | 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 (#) (u | 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:]
abs a is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of bool [:REAL,REAL:]
dom a is V45() V46() V47() Element of bool REAL
b is V22() real ext-real set
u is V22() real ext-real set
r is V22() real ext-real set
dom (abs a) is V45() V46() V47() Element of bool REAL
s is V22() real ext-real set
a . r is V22() real ext-real Element of REAL
a . s is V22() real ext-real Element of REAL
(a . r) - (a . s) is V22() real ext-real Element of REAL
abs ((a . r) - (a . s)) is V22() real ext-real Element of REAL
r - s is V22() real ext-real set
abs (r - s) is V22() real ext-real Element of REAL
u * (abs (r - s)) is V22() real ext-real Element of REAL
(abs a) . r is V22() real ext-real Element of REAL
(abs a) . s is V22() real ext-real Element of REAL
((abs a) . r) - ((abs a) . s) is V22() real ext-real Element of REAL
abs (((abs a) . r) - ((abs a) . s)) is V22() real ext-real Element of REAL
abs (a . r) is V22() real ext-real Element of REAL
(abs (a . r)) - ((abs a) . s) is V22() real ext-real Element of REAL
abs ((abs (a . r)) - ((abs a) . s)) is V22() real ext-real Element of REAL
abs (a . s) is V22() real ext-real Element of REAL
(abs (a . r)) - (abs (a . s)) is V22() real ext-real Element of REAL
abs ((abs (a . r)) - (abs (a . s))) is V22() real ext-real Element of REAL
u is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is V22() real ext-real set
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:]
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) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(- 1) (#) (b | a) is Relation-like REAL -defined Function-like complex-valued ext-real-valued real-valued set
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:]
(abs b) | a is Relation-like REAL -defined a -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below Element of bool [:REAL,REAL:]
abs (b | a) is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued bounded_below 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 V22() real ext-real set
dom a is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
a . b is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
(a . b) - (a . u) is V22() real ext-real Element of REAL
abs ((a . b) - (a . u)) is V22() real ext-real Element of REAL
b - u is V22() real ext-real set
abs (b - u) is V22() real ext-real Element of REAL
1 * (abs (b - u)) is V22() real ext-real Element of REAL
a is V45() V46() V47() Element of bool REAL
id a is Relation-like REAL -defined a -defined REAL -valued a -valued Function-like one-to-one total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
b is V22() real ext-real Element of REAL
dom (id a) is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
(id a) . u is V22() real ext-real Element of REAL
r is V22() real ext-real set
(id a) . r is V22() real ext-real Element of REAL
((id a) . u) - ((id a) . r) is V22() real ext-real Element of REAL
abs (((id a) . u) - ((id a) . r)) is V22() real ext-real Element of REAL
u - r is V22() real ext-real set
abs (u - r) is V22() real ext-real Element of REAL
b * (abs (u - r)) is V22() real ext-real Element of REAL
dom (id a) is V45() V46() V47() Element of bool a
bool a is set
u - ((id a) . r) is V22() real ext-real Element of REAL
abs (u - ((id a) . r)) is V22() real ext-real Element of REAL
b * (abs (u - r)) is V22() real ext-real Element of REAL
u 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:]
dom a is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
r is V22() real ext-real set
a . r is V22() real ext-real Element of REAL
s is V22() real ext-real set
s / u is V22() real ext-real Element of COMPLEX
r2 is V22() real ext-real Element of COMPLEX
x0 is V22() real ext-real set
x0 - r is V22() real ext-real set
abs (x0 - r) is V22() real ext-real Element of REAL
(s / u) * u is V22() real ext-real set
u * (abs (x0 - r)) is V22() real ext-real Element of REAL
a . x0 is V22() real ext-real Element of REAL
(a . x0) - (a . r) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . r)) is V22() real ext-real Element of REAL
u " is V22() real ext-real set
s * (u ") is V22() real ext-real set
x0 is V22() real ext-real set
x0 - r is V22() real ext-real set
abs (x0 - r) is V22() real ext-real Element of REAL
a . x0 is V22() real ext-real Element of REAL
(a . x0) - (a . r) is V22() real ext-real Element of REAL
abs ((a . x0) - (a . r)) 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:]
rng a is V45() V46() V47() Element of bool REAL
b is V22() real ext-real set
{b} is non empty trivial V45() V46() V47() Element of bool 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
a . r is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
(a . u) - (a . r) is V22() real ext-real Element of REAL
abs ((a . u) - (a . r)) is V22() real ext-real Element of REAL
u - r is V22() real ext-real set
abs (u - r) is V22() real ext-real Element of REAL
1 * (abs (u - r)) 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
u is V22() real ext-real set
a . b is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
(a . b) - (a . u) is V22() real ext-real Element of REAL
abs ((a . b) - (a . u)) is V22() real ext-real Element of REAL
b - u is V22() real ext-real set
abs (b - u) is V22() real ext-real Element of REAL
1 * (abs (b - u)) is V22() real ext-real Element of REAL
a is set
b is V22() real ext-real set
u is V22() real ext-real set
r is Relation-like REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r | 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:]
s is V22() real ext-real set
dom (r | a) is Element of bool a
bool a is set
r1 is V22() real ext-real set
r . r1 is V22() real ext-real Element of REAL
b * r1 is V22() real ext-real set
(b * r1) + u is V22() real ext-real set
s - r1 is V22() real ext-real set
abs (s - r1) is V22() real ext-real Element of REAL
r . s is V22() real ext-real Element of REAL
b * s is V22() real ext-real set
(b * s) + u is V22() real ext-real set
(r . s) - (r . r1) is V22() real ext-real Element of REAL
abs ((r . s) - (r . r1)) is V22() real ext-real Element of REAL
b * (s - r1) is V22() real ext-real set
abs (b * (s - r1)) is V22() real ext-real Element of REAL
abs b is V22() real ext-real Element of REAL
(abs b) * (abs (s - r1)) is V22() real ext-real Element of REAL
(abs ((r . s) - (r . r1))) + 0 is V22() real ext-real Element of REAL
1 * (abs (s - r1)) is V22() real ext-real Element of REAL
((abs b) * (abs (s - r1))) + (1 * (abs (s - r1))) is V22() real ext-real Element of REAL
(abs b) + 1 is V22() real ext-real Element of REAL
((abs b) + 1) * (abs (s - r1)) is V22() real ext-real Element of REAL
0 + 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 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
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
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:]
id (dom a) is Relation-like REAL -defined dom a -defined REAL -valued dom a -valued Function-like one-to-one total complex-valued ext-real-valued real-valued () () Element of bool [:REAL,REAL:]
u is set
a . u is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
r ^2 is V22() real ext-real Element of REAL
r * r 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 . r is V22() real ext-real Element of REAL
(b . r) * r is V22() real ext-real Element of REAL
b . u is V22() real ext-real Element of REAL
(b . u) * (b . u) is V22() real ext-real Element of REAL
dom b is V45() V46() V47() Element of bool REAL
(dom b) /\ (dom b) is V45() V46() V47() Element of bool REAL
b (#) 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 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:]
(dom b) /\ a is V45() V46() V47() Element of bool REAL
dom (b | a) is Element of bool a
bool a is set
u is V22() real ext-real set
b . u is V22() real ext-real Element of REAL
u ^2 is set
u * u is V22() real ext-real set
(b | a) . u is V22() real ext-real Element of 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:]
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
u is V22() real ext-real set
a . b is V22() real ext-real Element of REAL
abs b is V22() real ext-real Element of REAL
a . u is V22() real ext-real Element of REAL
abs u is V22() real ext-real Element of REAL
(a . b) - (a . u) is V22() real ext-real Element of REAL
abs ((a . b) - (a . u)) is V22() real ext-real Element of REAL
b - u is V22() real ext-real set
abs (b - u) is V22() real ext-real Element of REAL
1 * (abs (b - 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:]
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
dom (b | a) is Element of bool a
bool a is set
b . u is V22() real ext-real Element of REAL
abs u 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:]
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 is V45() V46() V47() Element of bool REAL
u is V22() real ext-real set
r is V22() real ext-real set
[.u,r.] is V45() V46() V47() V69() closed Element of bool REAL
s is V22() real ext-real Element of REAL
r1 is V22() real ext-real Element of REAL
{s} is non empty trivial V45() V46() V47() Element of bool REAL
rng (b | a) is V45() V46() V47() Element of bool REAL
r1 is V22() real ext-real Element of REAL
s is V22() real ext-real Element of 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:]
dom (b | a) is Element of bool a
bool a is set
[.s,r1.] is V45() V46() V47() V69() closed Element of bool REAL
].s,r1.[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
{s,r1} is non empty V45() V46() V47() set
].s,r1.[ \/ {s,r1} is non empty V45() V46() V47() set
r2 is V22() real ext-real set
(b | a) .: a is V45() V46() V47() Element of bool REAL
(b | a) . r2 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
(b | a) . x0 is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of (b | a) . x0
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V45() V46() V47() open Neighbourhood of (b | a) . x0
R is V22() real ext-real set
((b | a) . x0) - R is V22() real ext-real Element of REAL
((b | a) . x0) + R is V22() real ext-real Element of REAL
].(((b | a) . x0) - R),(((b | a) . x0) + R).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
x1 is V22() real ext-real Element of REAL
x1 / 2 is V22() real ext-real Element of REAL
((b | a) . x0) + (x1 / 2) is V22() real ext-real Element of REAL
(((b | a) . x0) + (x1 / 2)) + (x1 / 2) is V22() real ext-real Element of REAL
((b | a) . x0) + x1 is V22() real ext-real Element of REAL
(((b | a) . x0) + x1) - x1 is V22() real ext-real Element of REAL
((b | a) . x0) - x1 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= ((b | a) . x0) - x1 & not ((b | a) . x0) + x1 <= b1 ) } is set
].(((b | a) . x0) - x1),(((b | a) . x0) + x1).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V22() real ext-real Element of REAL
(b | a) . N is V22() real ext-real Element of REAL
((b | a) . x0) - (x1 / 2) is V22() real ext-real Element of REAL
(((b | a) . x0) - x1) + (x1 / 2) is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
(b | a) . x1 is V22() real ext-real Element of REAL
a /\ (dom (b | a)) is Element of bool a
N - x0 is V22() real ext-real Element of REAL
x0 - x1 is V22() real ext-real Element of REAL
min ((x0 - x1),(N - x0)) is V22() real ext-real Element of REAL
x0 - (min ((x0 - x1),(N - x0))) is V22() real ext-real Element of REAL
x0 + (min ((x0 - x1),(N - x0))) is V22() real ext-real Element of REAL
].(x0 - (min ((x0 - x1),(N - x0)))),(x0 + (min ((x0 - x1),(N - x0)))).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V45() V46() V47() open Neighbourhood of x0
x is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of x0
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x0 - (min ((x0 - x1),(N - x0))) & not x0 + (min ((x0 - x1),(N - x0))) <= b1 ) } is set
(min ((x0 - x1),(N - x0))) + x is V22() real ext-real Element of REAL
c22 is V22() real ext-real Element of REAL
((min ((x0 - x1),(N - x0))) + x) - x is V22() real ext-real Element of REAL
x0 - x is V22() real ext-real Element of REAL
- (x0 - x) is V22() real ext-real Element of REAL
- (x0 - x1) is V22() real ext-real Element of REAL
x - x0 is V22() real ext-real Element of REAL
(x - x0) + x0 is V22() real ext-real Element of REAL
x1 - x0 is V22() real ext-real Element of REAL
(x1 - x0) + x0 is V22() real ext-real Element of REAL
(b | a) . x is V22() real ext-real Element of REAL
c22 is V22() real ext-real Element of REAL
(N - x0) + x0 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( ((b | a) . x0) - (x1 / 2) <= b1 & b1 <= ((b | a) . x0) + (x1 / 2) ) } is set
[.(((b | a) . x0) - (x1 / 2)),(((b | a) . x0) + (x1 / 2)).] is V45() V46() V47() V69() closed Element of bool REAL
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V22() real ext-real set
s - N is V22() real ext-real Element of REAL
s + N is V22() real ext-real Element of REAL
].(s - N),(s + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V22() real ext-real Element of REAL
r1 - s is V22() real ext-real Element of REAL
min (N,(r1 - s)) is V22() real ext-real Element of REAL
(min (N,(r1 - s))) / 2 is V22() real ext-real Element of REAL
s + N is V22() real ext-real Element of REAL
s + ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
s - ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- N is V22() real ext-real Element of REAL
s + (- ((min (N,(r1 - s))) / 2)) is V22() real ext-real Element of REAL
s + (- N) is V22() real ext-real Element of REAL
s - N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= s - N & not s + N <= b1 ) } is set
].(s - N),(s + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= s & not r1 <= b1 ) } is set
x1 is V22() real ext-real Element of REAL
(b | a) . x1 is V22() real ext-real Element of REAL
a /\ (dom (b | a)) is Element of bool a
x1 - x0 is V22() real ext-real Element of REAL
x0 - (x1 - x0) is V22() real ext-real Element of REAL
x0 + (x1 - x0) is V22() real ext-real Element of REAL
].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V45() V46() V47() open Neighbourhood of x0
x is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of x0
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x0 - (x1 - x0) & not x0 + (x1 - x0) <= b1 ) } is set
(b | a) . x is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( s <= b1 & b1 <= r1 ) } is set
x1 is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( s - ((min (N,(r1 - s))) / 2) <= b1 & b1 <= s + ((min (N,(r1 - s))) / 2) ) } is set
[.(s - ((min (N,(r1 - s))) / 2)),(s + ((min (N,(r1 - s))) / 2)).] is V45() V46() V47() V69() closed Element of bool REAL
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V22() real ext-real set
r1 - N is V22() real ext-real Element of REAL
r1 + N is V22() real ext-real Element of REAL
].(r1 - N),(r1 + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V22() real ext-real Element of REAL
r1 - s is V22() real ext-real Element of REAL
min (N,(r1 - s)) is V22() real ext-real Element of REAL
(min (N,(r1 - s))) / 2 is V22() real ext-real Element of REAL
r1 - ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
((min (N,(r1 - s))) / 2) + s is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= s & not r1 <= b1 ) } is set
x1 is V22() real ext-real Element of REAL
(b | a) . x1 is V22() real ext-real Element of REAL
a /\ (dom (b | a)) is Element of bool a
r1 + N is V22() real ext-real Element of REAL
r1 + ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- N is V22() real ext-real Element of REAL
r1 + (- ((min (N,(r1 - s))) / 2)) is V22() real ext-real Element of REAL
r1 + (- N) is V22() real ext-real Element of REAL
r1 - N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= r1 - N & not r1 + N <= b1 ) } is set
].(r1 - N),(r1 + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
x0 - x1 is V22() real ext-real Element of REAL
x0 - (x0 - x1) is V22() real ext-real Element of REAL
x0 + (x0 - x1) is V22() real ext-real Element of REAL
].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V45() V46() V47() open Neighbourhood of x0
x is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of x0
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x0 - (x0 - x1) & not x0 + (x0 - x1) <= b1 ) } is set
(b | a) . x is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( s <= b1 & b1 <= r1 ) } is set
x1 is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( r1 - ((min (N,(r1 - s))) / 2) <= b1 & b1 <= r1 + ((min (N,(r1 - s))) / 2) ) } is set
[.(r1 - ((min (N,(r1 - s))) / 2)),(r1 + ((min (N,(r1 - s))) / 2)).] is V45() V46() V47() V69() closed Element of bool REAL
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V45() V46() V47() open Neighbourhood of x0
N is V45() V46() V47() open Neighbourhood of x0
N is V45() V46() V47() open Neighbourhood of x0
R is V22() real ext-real set
(b | a) . R is V22() real ext-real Element of 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:]
dom (b | a) is Element of bool a
bool a is set
[.s,r1.] is V45() V46() V47() V69() closed Element of bool REAL
].s,r1.[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
{s,r1} is non empty V45() V46() V47() set
].s,r1.[ \/ {s,r1} is non empty V45() V46() V47() set
r2 is V22() real ext-real set
(b | a) .: a is V45() V46() V47() Element of bool REAL
(b | a) . r2 is V22() real ext-real Element of REAL
x0 is V22() real ext-real Element of REAL
(b | a) . x0 is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of (b | a) . x0
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V45() V46() V47() open Neighbourhood of (b | a) . x0
R is V22() real ext-real set
((b | a) . x0) - R is V22() real ext-real Element of REAL
((b | a) . x0) + R is V22() real ext-real Element of REAL
].(((b | a) . x0) - R),(((b | a) . x0) + R).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
x1 is V22() real ext-real Element of REAL
x1 / 2 is V22() real ext-real Element of REAL
((b | a) . x0) + (x1 / 2) is V22() real ext-real Element of REAL
(((b | a) . x0) + (x1 / 2)) + (x1 / 2) is V22() real ext-real Element of REAL
((b | a) . x0) + x1 is V22() real ext-real Element of REAL
(((b | a) . x0) + x1) - x1 is V22() real ext-real Element of REAL
((b | a) . x0) - x1 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= ((b | a) . x0) - x1 & not ((b | a) . x0) + x1 <= b1 ) } is set
].(((b | a) . x0) - x1),(((b | a) . x0) + x1).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V22() real ext-real Element of REAL
(b | a) . N is V22() real ext-real Element of REAL
((b | a) . x0) - (x1 / 2) is V22() real ext-real Element of REAL
(((b | a) . x0) - x1) + (x1 / 2) is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
(b | a) . x1 is V22() real ext-real Element of REAL
a /\ (dom (b | a)) is Element of bool a
x0 - N is V22() real ext-real Element of REAL
x1 - x0 is V22() real ext-real Element of REAL
min ((x1 - x0),(x0 - N)) is V22() real ext-real Element of REAL
x0 - (min ((x1 - x0),(x0 - N))) is V22() real ext-real Element of REAL
x0 + (min ((x1 - x0),(x0 - N))) is V22() real ext-real Element of REAL
].(x0 - (min ((x1 - x0),(x0 - N)))),(x0 + (min ((x1 - x0),(x0 - N)))).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V45() V46() V47() open Neighbourhood of x0
x is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of x0
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x0 - (min ((x1 - x0),(x0 - N))) & not x0 + (min ((x1 - x0),(x0 - N))) <= b1 ) } is set
(min ((x1 - x0),(x0 - N))) + x is V22() real ext-real Element of REAL
c22 is V22() real ext-real Element of REAL
((min ((x1 - x0),(x0 - N))) + x) - x is V22() real ext-real Element of REAL
x0 - x is V22() real ext-real Element of REAL
x - x0 is V22() real ext-real Element of REAL
c22 is V22() real ext-real Element of REAL
(x1 - x0) + x0 is V22() real ext-real Element of REAL
(x - x0) + x0 is V22() real ext-real Element of REAL
(b | a) . x is V22() real ext-real Element of REAL
- (x0 - x) is V22() real ext-real Element of REAL
- (x0 - N) is V22() real ext-real Element of REAL
N - x0 is V22() real ext-real Element of REAL
(N - x0) + x0 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( ((b | a) . x0) - (x1 / 2) <= b1 & b1 <= ((b | a) . x0) + (x1 / 2) ) } is set
[.(((b | a) . x0) - (x1 / 2)),(((b | a) . x0) + (x1 / 2)).] is V45() V46() V47() V69() closed Element of bool REAL
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V22() real ext-real set
s - N is V22() real ext-real Element of REAL
s + N is V22() real ext-real Element of REAL
].(s - N),(s + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V22() real ext-real Element of REAL
r1 - s is V22() real ext-real Element of REAL
min (N,(r1 - s)) is V22() real ext-real Element of REAL
(min (N,(r1 - s))) / 2 is V22() real ext-real Element of REAL
s + N is V22() real ext-real Element of REAL
s + ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
s - ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- N is V22() real ext-real Element of REAL
s + (- ((min (N,(r1 - s))) / 2)) is V22() real ext-real Element of REAL
s + (- N) is V22() real ext-real Element of REAL
s - N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= s - N & not s + N <= b1 ) } is set
].(s - N),(s + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= s & not r1 <= b1 ) } is set
x1 is V22() real ext-real Element of REAL
(b | a) . x1 is V22() real ext-real Element of REAL
a /\ (dom (b | a)) is Element of bool a
x0 - x1 is V22() real ext-real Element of REAL
x0 - (x0 - x1) is V22() real ext-real Element of REAL
x0 + (x0 - x1) is V22() real ext-real Element of REAL
].(x0 - (x0 - x1)),(x0 + (x0 - x1)).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V45() V46() V47() open Neighbourhood of x0
x is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of x0
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x0 - (x0 - x1) & not x0 + (x0 - x1) <= b1 ) } is set
(b | a) . x is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( s <= b1 & b1 <= r1 ) } is set
x1 is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( s - ((min (N,(r1 - s))) / 2) <= b1 & b1 <= s + ((min (N,(r1 - s))) / 2) ) } is set
[.(s - ((min (N,(r1 - s))) / 2)),(s + ((min (N,(r1 - s))) / 2)).] is V45() V46() V47() V69() closed Element of bool REAL
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V22() real ext-real set
r1 - N is V22() real ext-real Element of REAL
r1 + N is V22() real ext-real Element of REAL
].(r1 - N),(r1 + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V22() real ext-real Element of REAL
r1 - s is V22() real ext-real Element of REAL
min (N,(r1 - s)) is V22() real ext-real Element of REAL
(min (N,(r1 - s))) / 2 is V22() real ext-real Element of REAL
r1 - ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
((min (N,(r1 - s))) / 2) + s is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= s & not r1 <= b1 ) } is set
x1 is V22() real ext-real Element of REAL
(b | a) . x1 is V22() real ext-real Element of REAL
a /\ (dom (b | a)) is Element of bool a
r1 + N is V22() real ext-real Element of REAL
r1 + ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- ((min (N,(r1 - s))) / 2) is V22() real ext-real Element of REAL
- N is V22() real ext-real Element of REAL
r1 + (- ((min (N,(r1 - s))) / 2)) is V22() real ext-real Element of REAL
r1 + (- N) is V22() real ext-real Element of REAL
r1 - N is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= r1 - N & not r1 + N <= b1 ) } is set
].(r1 - N),(r1 + N).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
x1 - x0 is V22() real ext-real Element of REAL
x0 - (x1 - x0) is V22() real ext-real Element of REAL
x0 + (x1 - x0) is V22() real ext-real Element of REAL
].(x0 - (x1 - x0)),(x0 + (x1 - x0)).[ is V45() V46() V47() V64() V65() V69() open Element of bool REAL
N is V45() V46() V47() open Neighbourhood of x0
x is V22() real ext-real Element of REAL
N is V45() V46() V47() open Neighbourhood of x0
{ b1 where b1 is V22() real ext-real Element of REAL : ( not b1 <= x0 - (x1 - x0) & not x0 + (x1 - x0) <= b1 ) } is set
(b | a) . x is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( s <= b1 & b1 <= r1 ) } is set
x1 is V22() real ext-real Element of REAL
x1 is V22() real ext-real Element of REAL
{ b1 where b1 is V22() real ext-real Element of REAL : ( r1 - ((min (N,(r1 - s))) / 2) <= b1 & b1 <= r1 + ((min (N,(r1 - s))) / 2) ) } is set
[.(r1 - ((min (N,(r1 - s))) / 2)),(r1 + ((min (N,(r1 - s))) / 2)).] is V45() V46() V47() V69() closed Element of bool REAL
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N1 is V45() V46() V47() open Neighbourhood of (b | a) . x0
N is V45() V46() V47() open Neighbourhood of x0
N is V45() V46() V47() open Neighbourhood of x0
N is V45() V46() V47() open Neighbourhood of x0
R is V22() real ext-real set
(b | a) . R is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
r1 is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is V22() real ext-real set
[.a,b.] is V45() V46() V47() V69() closed Element of bool REAL
u is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
dom u is V45() V46() V47() Element of bool REAL
u | [.a,b.] is Relation-like REAL -defined [.a,b.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | [.a,b.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u .: [.a,b.] is V45() V46() V47() Element of bool REAL
((u | [.a,b.]) ") | (u .: [.a,b.]) is Relation-like REAL -defined u .: [.a,b.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.r,s.] is V45() V46() V47() V69() closed Element of bool REAL
u | [.r,s.] is Relation-like REAL -defined [.r,s.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | [.r,s.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u .: [.r,s.] is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") .: (u .: [.r,s.]) is V45() V46() V47() Element of bool REAL
rng (u | [.r,s.]) is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") .: (rng (u | [.r,s.])) is V45() V46() V47() Element of bool REAL
dom ((u | [.r,s.]) ") is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") .: (dom ((u | [.r,s.]) ")) is V45() V46() V47() Element of bool REAL
rng ((u | [.r,s.]) ") is V45() V46() V47() Element of bool REAL
dom (u | [.r,s.]) is V45() V46() V47() Element of bool REAL
(dom u) /\ [.r,s.] is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") | (u .: [.r,s.]) is Relation-like REAL -defined u .: [.r,s.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.r,s.] is V45() V46() V47() V69() closed Element of bool REAL
u | [.r,s.] is Relation-like REAL -defined [.r,s.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(u | [.r,s.]) " is Relation-like REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
u .: [.r,s.] is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") .: (u .: [.r,s.]) is V45() V46() V47() Element of bool REAL
rng (u | [.r,s.]) is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") .: (rng (u | [.r,s.])) is V45() V46() V47() Element of bool REAL
dom ((u | [.r,s.]) ") is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") .: (dom ((u | [.r,s.]) ")) is V45() V46() V47() Element of bool REAL
rng ((u | [.r,s.]) ") is V45() V46() V47() Element of bool REAL
dom (u | [.r,s.]) is V45() V46() V47() Element of bool REAL
(dom u) /\ [.r,s.] is V45() V46() V47() Element of bool REAL
((u | [.r,s.]) ") | (u .: [.r,s.]) is Relation-like REAL -defined u .: [.r,s.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is V22() real ext-real Element of REAL
s is V22() real ext-real Element of REAL
[.r,s.] is V45() V46() V47() V69() closed Element of bool REAL
u | [.r,s.] is Relation-like REAL -defined [.r,s.] -defined REAL -defined REAL -valued Function-like one-to-one complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
a is V22() real ext-real set
b is V22() real ext-real set
u is V22() real ext-real Element of REAL
r is V22() real ext-real Element of REAL
s is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r1 is V22() real ext-real set
s . r1 is V22() real ext-real Element of REAL
a * r1 is V22() real ext-real set
(a * r1) + b is V22() real ext-real set
r2 is V22() real ext-real Element of REAL
s . r2 is V22() real ext-real Element of REAL
u * r1 is V22() real ext-real Element of REAL
(u * r1) + r is V22() real ext-real Element of REAL
u is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
s is V22() real ext-real Element of REAL
u . s is V22() real ext-real Element of REAL
a * s is V22() real ext-real Element of REAL
(a * s) + b is V22() real ext-real Element of REAL
r . s is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
r is V22() real ext-real set
(a,b) . r is V22() real ext-real Element of REAL
a * r is V22() real ext-real set
(a * r) + b is V22() real ext-real set
dom (a,b) is non empty V45() V46() V47() Element of bool REAL
(a,b) | REAL is Relation-like REAL -defined REAL -defined REAL -valued Function-like complex-valued ext-real-valued real-valued Element of bool [:REAL,REAL:]
(1,1) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) . 0 is V22() real ext-real Element of REAL
a * 0 is V22() real ext-real Element of REAL
(a * 0) + b is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) . 1 is V22() real ext-real Element of REAL
a + b is V22() real ext-real set
a * 1 is V22() real ext-real Element of REAL
(a * 1) + b is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
u is set
dom (a,b) is non empty set
r is set
(a,b) . u is V22() real ext-real set
(a,b) . r is V22() real ext-real set
dom (a,b) is non empty V45() V46() V47() Element of bool REAL
(a,b) . u is V22() real ext-real Element of REAL
(a,b) . r is V22() real ext-real Element of REAL
r1 is V22() real ext-real set
a * r1 is V22() real ext-real set
(a * r1) + b is V22() real ext-real set
r2 is V22() real ext-real set
a * r2 is V22() real ext-real set
(a * r2) + b is V22() real ext-real set
a is V22() real ext-real set
r is V22() real ext-real set
u is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) . r is V22() real ext-real Element of REAL
(a,b) . u is V22() real ext-real Element of REAL
a * r is V22() real ext-real set
a * u is V22() real ext-real set
(a * u) + b is V22() real ext-real set
(a * r) + b is V22() real ext-real set
a is V22() real ext-real set
r is V22() real ext-real set
u is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) . u is V22() real ext-real Element of REAL
(a,b) . r is V22() real ext-real Element of REAL
a * u is V22() real ext-real set
a * r is V22() real ext-real set
(a * u) + b is V22() real ext-real set
(a * r) + b is V22() real ext-real set
a is V22() real ext-real set
u is V22() real ext-real set
r is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) . u is V22() real ext-real Element of REAL
(a,b) . r is V22() real ext-real Element of REAL
a * u is V22() real ext-real set
a * r is V22() real ext-real set
(a * u) + b is V22() real ext-real set
(a * r) + b is V22() real ext-real set
a is V22() real ext-real set
u is V22() real ext-real set
r is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) . r is V22() real ext-real Element of REAL
(a,b) . u is V22() real ext-real Element of REAL
a * r is V22() real ext-real set
a * u is V22() real ext-real set
(a * u) + b is V22() real ext-real set
(a * r) + b is V22() real ext-real set
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
rng (a,b) is non empty V45() V46() V47() Element of bool REAL
u is set
r is V22() real ext-real Element of REAL
r - b is V22() real ext-real Element of REAL
(r - b) / a is V22() real ext-real Element of REAL
(a,b) . ((r - b) / a) is V22() real ext-real Element of REAL
a * ((r - b) / a) is V22() real ext-real Element of REAL
(a * ((r - b) / a)) + b is V22() real ext-real Element of REAL
(r - b) + b is V22() real ext-real Element of REAL
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) " is Relation-like Function-like set
a " is V22() real ext-real set
b / a is V22() real ext-real Element of COMPLEX
- (b / a) is V22() real ext-real Element of COMPLEX
((a "),(- (b / a))) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
((a "),(- (b / a))) * (a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
id REAL is Relation-like REAL -defined REAL -valued Function-like one-to-one non empty total quasi_total complex-valued ext-real-valued real-valued increasing non-decreasing monotone Element of bool [:REAL,REAL:]
u is V22() real ext-real Element of REAL
(((a "),(- (b / a))) * (a,b)) . u is V22() real ext-real Element of REAL
(id REAL) . u is V22() real ext-real Element of REAL
(a,b) . u is V22() real ext-real Element of REAL
((a "),(- (b / a))) . ((a,b) . u) is V22() real ext-real Element of REAL
a * u is V22() real ext-real Element of REAL
(a * u) + b is V22() real ext-real Element of REAL
((a "),(- (b / a))) . ((a * u) + b) is V22() real ext-real Element of REAL
(a ") * ((a * u) + b) is V22() real ext-real Element of REAL
((a ") * ((a * u) + b)) + (- (b / a)) is V22() real ext-real Element of REAL
(a ") * a is V22() real ext-real set
((a ") * a) * u is V22() real ext-real Element of REAL
(a ") * b is V22() real ext-real set
(((a ") * a) * u) + ((a ") * b) is V22() real ext-real Element of REAL
((((a ") * a) * u) + ((a ") * b)) + (- (b / a)) is V22() real ext-real Element of REAL
1 * u is V22() real ext-real Element of REAL
(1 * u) + ((a ") * b) is V22() real ext-real Element of REAL
((1 * u) + ((a ") * b)) + (- (b / a)) is V22() real ext-real Element of REAL
u + ((a ") * b) is V22() real ext-real Element of REAL
(u + ((a ") * b)) - (b / a) is V22() real ext-real Element of REAL
u + (b / a) is V22() real ext-real Element of REAL
(u + (b / a)) - (b / a) is V22() real ext-real Element of REAL
rng (a,b) is non empty V45() V46() V47() Element of bool REAL
[.0,1.] is V45() V46() V47() V69() closed Element of bool REAL
a is V22() real ext-real set
b is V22() real ext-real set
(a,b) is Relation-like REAL -defined REAL -valued Function-like non empty total quasi_total complex-valued ext-real-valued real-valued () Element of bool [:REAL,REAL:]
(a,b) .: [.0,1.] is V45() V46() V47() Element of bool REAL
a + b is V22() real ext-real set
[.b,(a + b).] is V45() V46() V47() V69() closed Element of bool REAL
(a,b) . 1 is V22() real ext-real Element of REAL
u is set
r is V22() real ext-real Element of REAL
(a,b) . r is V22() real ext-real Element of REAL
s is V22() real ext-real set
(a,b) . 0 is V22() real ext-real Element of REAL
u is set
r is V22() real ext-real Element of REAL
r - b is V22() real ext-real Element of REAL
(r - b) / a is V22() real ext-real Element of REAL
(a,b) . ((r - b) / a) is V22() real ext-real Element of REAL
a * ((r - b) / a) is V22() real ext-real Element of REAL
(a * ((r - b) / a)) + b is V22() real ext-real Element of REAL
(r - b) + b is V22() real ext-real Element of REAL
a / a is V22() real ext-real Element of COMPLEX