:: MESFUNC1 semantic presentation

REAL is non empty V35() V59() V60() V61() V65() set
NAT is epsilon-transitive epsilon-connected ordinal non empty V35() cardinal limit_cardinal V59() V60() V61() V62() V63() V64() V65() Element of bool REAL
bool REAL is non empty V35() set
ExtREAL is non empty V60() set
[:NAT,ExtREAL:] is non empty V35() ext-real-valued set
bool [:NAT,ExtREAL:] is non empty V35() set
bool ExtREAL is non empty set
omega is epsilon-transitive epsilon-connected ordinal non empty V35() cardinal limit_cardinal V59() V60() V61() V62() V63() V64() V65() set
bool omega is non empty V35() set
[:NAT,REAL:] is non empty V35() complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty V35() set
bool (bool REAL) is non empty V35() set
COMPLEX is non empty V35() V59() V65() set
RAT is non empty V35() V59() V60() V61() V62() V65() set
INT is non empty V35() V59() V60() V61() V62() V63() V65() set
bool NAT is non empty V35() set
[:COMPLEX,COMPLEX:] is non empty V35() complex-valued set
bool [:COMPLEX,COMPLEX:] is non empty V35() set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V35() complex-valued set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V35() set
[:REAL,REAL:] is non empty V35() complex-valued ext-real-valued real-valued set
bool [:REAL,REAL:] is non empty V35() set
[:[:REAL,REAL:],REAL:] is non empty V35() complex-valued ext-real-valued real-valued set
bool [:[:REAL,REAL:],REAL:] is non empty V35() set
[:RAT,RAT:] is RAT -valued non empty V35() complex-valued ext-real-valued real-valued set
bool [:RAT,RAT:] is non empty V35() set
[:[:RAT,RAT:],RAT:] is RAT -valued non empty V35() complex-valued ext-real-valued real-valued set
bool [:[:RAT,RAT:],RAT:] is non empty V35() set
[:INT,INT:] is RAT -valued INT -valued non empty V35() complex-valued ext-real-valued real-valued set
bool [:INT,INT:] is non empty V35() set
[:[:INT,INT:],INT:] is RAT -valued INT -valued non empty V35() complex-valued ext-real-valued real-valued set
bool [:[:INT,INT:],INT:] is non empty V35() set
[:NAT,NAT:] is RAT -valued INT -valued non empty V35() complex-valued ext-real-valued real-valued natural-valued set
[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non empty V35() complex-valued ext-real-valued real-valued natural-valued set
bool [:[:NAT,NAT:],NAT:] is non empty V35() set
{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() set
1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer rational V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of NAT
card omega is epsilon-transitive epsilon-connected ordinal non empty V35() cardinal set
+infty is non empty non real ext-real positive non negative set
-infty is non empty non real ext-real non positive negative set
X is V59() V60() V61() Element of bool REAL
S is V16() real ext-real Element of REAL
f is V16() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- A is V16() real ext-real non positive integer Element of REAL
X is V59() V60() V61() Element of bool REAL
S is V59() V60() V61() Element of bool REAL
f is V16() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- A is V16() real ext-real non positive integer Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- A is V16() real ext-real non positive integer Element of REAL
() is V59() V60() V61() Element of bool REAL
- 0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of REAL
X is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- X is V16() real ext-real non positive integer Element of REAL
[:NAT,():] is non empty V35() complex-valued ext-real-valued real-valued set
bool [:NAT,():] is non empty V35() set
X is Relation-like NAT -defined () -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:NAT,():]
Funcs (NAT,()) is non empty FUNCTION_DOMAIN of NAT ,()
dom X is set
S is set
f is set
X . S is V16() real ext-real Element of ExtREAL
X . f is V16() real ext-real Element of ExtREAL
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
X . A is V16() real ext-real Element of ExtREAL
- A is V16() real ext-real non positive integer Element of REAL
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
X . r is V16() real ext-real Element of ExtREAL
- r is V16() real ext-real non positive integer Element of REAL
- (- A) is V16() real ext-real non negative integer Element of REAL
S is set
{S} is non empty trivial 1 -element set
X " {S} is set
f is V16() real ext-real Element of REAL
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- A is V16() real ext-real non positive integer Element of REAL
X . A is V16() real ext-real Element of ExtREAL
{f} is non empty trivial 1 -element V59() V60() V61() set
rng X is V59() V60() V61() set
() \/ NAT is non empty V59() V60() V61() Element of bool REAL
X is set
S is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- S is V16() real ext-real non positive integer Element of REAL
X is set
S is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- S is V16() real ext-real non positive integer Element of REAL
bool RAT is non empty V35() set
X is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer V35() cardinal set
S is V59() V60() V61() V62() Element of bool RAT
f is rational set
A is V16() real ext-real rational Element of RAT
r is V16() real ext-real integer set
r / X is V16() real ext-real set
r is V16() real ext-real integer set
r / X is V16() real ext-real set
r1 is V16() real ext-real integer set
r1 / X is V16() real ext-real set
f is rational set
A is rational set
r is V16() real ext-real integer set
r / X is V16() real ext-real set
S is V59() V60() V61() V62() Element of bool RAT
f is V59() V60() V61() V62() Element of bool RAT
A is V16() real ext-real rational Element of RAT
r is rational set
r1 is V16() real ext-real integer set
r1 / X is V16() real ext-real set
r is rational set
r1 is V16() real ext-real integer set
r1 / X is V16() real ext-real set
X is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer V35() cardinal set
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
((X + 1)) is V59() V60() V61() V62() Element of bool RAT
S is V16() real ext-real integer set
0 / S is V16() real ext-real Element of REAL
f is rational set
X is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer V35() cardinal set
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
((X + 1)) is non empty V59() V60() V61() V62() Element of bool RAT
S is V16() real ext-real integer rational Element of INT
S / (X + 1) is V16() real ext-real Element of REAL
f is V16() real ext-real integer set
A is V16() real ext-real integer set
f / A is V16() real ext-real set
r1 is rational set
[:INT,((X + 1)):] is RAT -valued non empty V35() complex-valued ext-real-valued real-valued set
bool [:INT,((X + 1)):] is non empty V35() set
S is Relation-like INT -defined ((X + 1)) -valued Function-like quasi_total complex-valued ext-real-valued real-valued Element of bool [:INT,((X + 1)):]
Funcs (INT,((X + 1))) is non empty FUNCTION_DOMAIN of INT ,((X + 1))
dom S is set
f is set
A is set
S . f is V16() real ext-real Element of ExtREAL
S . A is V16() real ext-real Element of ExtREAL
r is V16() real ext-real integer rational Element of INT
S . r is V16() real ext-real Element of ExtREAL
r / (X + 1) is V16() real ext-real Element of REAL
r1 is V16() real ext-real integer rational Element of INT
S . r1 is V16() real ext-real Element of ExtREAL
r1 / (X + 1) is V16() real ext-real Element of REAL
f is set
{f} is non empty trivial 1 -element set
S " {f} is set
A is rational set
r is V16() real ext-real integer set
r / (X + 1) is V16() real ext-real Element of REAL
r1 is V16() real ext-real integer rational Element of INT
S . r1 is V16() real ext-real Element of ExtREAL
r1 / (X + 1) is V16() real ext-real Element of REAL
{A} is non empty trivial 1 -element V59() V60() V61() V62() set
rng S is V59() V60() V61() set
X is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
X + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
((X + 1)) is non empty V59() V60() V61() V62() Element of bool RAT
S is set
S is V59() V60() V61() Element of bool REAL
[:NAT,(bool REAL):] is non empty V35() set
bool [:NAT,(bool REAL):] is non empty V35() set
X is Relation-like NAT -defined bool REAL -valued Function-like quasi_total Element of bool [:NAT,(bool REAL):]
rng X is set
union (rng X) is set
S is set
f is set
dom X is set
A is set
X . A is set
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
((r + 1)) is non empty V59() V60() V61() V62() Element of bool RAT
S is set
dom X is set
f is rational set
denominator f is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer V35() cardinal set
A + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(denominator f) - 1 is V16() real ext-real integer Element of REAL
numerator f is V16() real ext-real integer set
r1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(numerator f) / (r1 + 1) is V16() real ext-real Element of REAL
((r1 + 1)) is non empty V59() V60() V61() V62() Element of bool RAT
X . r1 is V59() V60() V61() Element of bool REAL
dom X is set
S is set
f is set
X . f is set
A is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
A + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
((A + 1)) is non empty V59() V60() V61() V62() Element of bool RAT
card NAT is epsilon-transitive epsilon-connected ordinal non empty V35() cardinal set
card S is epsilon-transitive epsilon-connected ordinal cardinal set
card RAT is epsilon-transitive epsilon-connected ordinal non empty V35() cardinal set
X is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
dom S is set
dom f is set
(dom S) /\ (dom f) is set
-infty is non empty non real ext-real non positive negative Element of ExtREAL
{-infty} is non empty trivial 1 -element V60() set
S " {-infty} is set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
{+infty} is non empty trivial 1 -element V60() set
f " {+infty} is set
(S " {-infty}) /\ (f " {+infty}) is set
S " {+infty} is set
f " {-infty} is set
(S " {+infty}) /\ (f " {-infty}) is set
((S " {-infty}) /\ (f " {+infty})) \/ ((S " {+infty}) /\ (f " {-infty})) is set
((dom S) /\ (dom f)) \ (((S " {-infty}) /\ (f " {+infty})) \/ ((S " {+infty}) /\ (f " {-infty}))) is Element of bool ((dom S) /\ (dom f))
bool ((dom S) /\ (dom f)) is non empty set
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is set
r1 is Element of X
r is set
r1 is Element of X
r is Element of X
A . r is ext-real Element of ExtREAL
S . r is ext-real Element of ExtREAL
f . r is ext-real Element of ExtREAL
(S . r) + (f . r) is ext-real Element of ExtREAL
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
dom r is set
r1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
dom r1 is set
(dom r) /\ (dom r1) is set
r " {-infty} is set
r1 " {+infty} is set
(r " {-infty}) /\ (r1 " {+infty}) is set
r " {+infty} is set
r1 " {-infty} is set
(r " {+infty}) /\ (r1 " {-infty}) is set
((r " {-infty}) /\ (r1 " {+infty})) \/ ((r " {+infty}) /\ (r1 " {-infty})) is set
((dom r) /\ (dom r1)) \ (((r " {-infty}) /\ (r1 " {+infty})) \/ ((r " {+infty}) /\ (r1 " {-infty}))) is Element of bool ((dom r) /\ (dom r1))
bool ((dom r) /\ (dom r1)) is non empty set
(dom r1) /\ (dom r) is set
(r1 " {-infty}) /\ (r " {+infty}) is set
(r1 " {+infty}) /\ (r " {-infty}) is set
((r1 " {-infty}) /\ (r " {+infty})) \/ ((r1 " {+infty}) /\ (r " {-infty})) is set
((dom r1) /\ (dom r)) \ (((r1 " {-infty}) /\ (r " {+infty})) \/ ((r1 " {+infty}) /\ (r " {-infty}))) is Element of bool ((dom r1) /\ (dom r))
bool ((dom r1) /\ (dom r)) is non empty set
x1 is Element of X
A . x1 is ext-real Element of ExtREAL
r1 . x1 is ext-real Element of ExtREAL
r . x1 is ext-real Element of ExtREAL
(r1 . x1) + (r . x1) is ext-real Element of ExtREAL
(S " {+infty}) /\ (f " {+infty}) is set
(S " {-infty}) /\ (f " {-infty}) is set
((S " {+infty}) /\ (f " {+infty})) \/ ((S " {-infty}) /\ (f " {-infty})) is set
((dom S) /\ (dom f)) \ (((S " {+infty}) /\ (f " {+infty})) \/ ((S " {-infty}) /\ (f " {-infty}))) is Element of bool ((dom S) /\ (dom f))
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is set
r1 is Element of X
r is set
r1 is Element of X
r is Element of X
A . r is ext-real Element of ExtREAL
S . r is ext-real Element of ExtREAL
f . r is ext-real Element of ExtREAL
(S . r) - (f . r) is ext-real Element of ExtREAL
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is set
r1 is Element of X
r is set
r1 is Element of X
r is Element of X
A . r is ext-real Element of ExtREAL
S . r is ext-real Element of ExtREAL
f . r is ext-real Element of ExtREAL
(S . r) * (f . r) is ext-real Element of ExtREAL
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
dom r is set
r1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
dom r1 is set
(dom r) /\ (dom r1) is set
(dom r1) /\ (dom r) is set
x1 is Element of X
A . x1 is ext-real Element of ExtREAL
r1 . x1 is ext-real Element of ExtREAL
r . x1 is ext-real Element of ExtREAL
(r1 . x1) * (r . x1) is ext-real Element of ExtREAL
X is non empty set
f is V16() real ext-real Element of REAL
R_EAL f is ext-real Element of ExtREAL
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
dom S is set
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is set
r1 is Element of X
r is set
r1 is Element of X
r is Element of X
A . r is ext-real Element of ExtREAL
S . r is ext-real Element of ExtREAL
(R_EAL f) * (S . r) is ext-real Element of ExtREAL
X is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is V16() real ext-real Element of REAL
(X,S,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (X,S,f) is set
R_EAL f is ext-real Element of ExtREAL
A is Element of X
S . A is ext-real Element of ExtREAL
(X,S,f) . A is ext-real Element of ExtREAL
((X,S,f) . A) / (R_EAL f) is ext-real Element of ExtREAL
(R_EAL f) * (S . A) is ext-real Element of ExtREAL
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
r is V16() real ext-real Element of REAL
f * r is V16() real ext-real Element of REAL
(f * r) / f is V16() real ext-real Element of REAL
f / f is V16() real ext-real Element of REAL
r / (f / f) is V16() real ext-real Element of REAL
r / 1 is V16() real ext-real Element of REAL
X is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
dom S is set
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
A is set
r is Element of X
A is set
r is Element of X
A is Element of X
f . A is ext-real Element of ExtREAL
S . A is ext-real Element of ExtREAL
- (S . A) is ext-real Element of ExtREAL
() is ext-real Element of ExtREAL
X is non empty set
f is V16() real ext-real Element of REAL
R_EAL f is ext-real Element of ExtREAL
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
dom S is set
0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty V16() real ext-real non positive non negative Function-like functional integer V35() cardinal {} -element V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
{0.} is non empty trivial 1 -element V59() V60() V61() V62() V63() V64() set
S " {0.} is set
(dom S) \ (S " {0.}) is Element of bool (dom S)
bool (dom S) is non empty set
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is set
r1 is Element of X
r is set
r1 is Element of X
r is Element of X
A . r is ext-real Element of ExtREAL
S . r is ext-real Element of ExtREAL
(R_EAL f) / (S . r) is ext-real Element of ExtREAL
X is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,S,1) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom (X,S,1) is set
dom S is set
S " {0.} is set
(dom S) \ (S " {0.}) is Element of bool (dom S)
bool (dom S) is non empty set
f is Element of X
(X,S,1) . f is ext-real Element of ExtREAL
S . f is ext-real Element of ExtREAL
() / (S . f) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
(R_EAL 1) / (S . f) is ext-real Element of ExtREAL
X is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
dom S is set
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
A is set
r is Element of X
A is set
r is Element of X
A is Element of X
f . A is ext-real Element of ExtREAL
S . A is ext-real Element of ExtREAL
|.(S . A).| is ext-real Element of ExtREAL
X is V16() real ext-real Element of REAL
[/X\] is V16() real ext-real integer set
S is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
[/X\] is V16() real ext-real integer set
[/X\] is V16() real ext-real integer set
X is V16() real ext-real Element of REAL
[\X/] is V16() real ext-real integer set
S is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- f is V16() real ext-real non positive integer Element of REAL
S is V16() real ext-real set
X is V16() real ext-real set
S - X is V16() real ext-real set
f is V16() real ext-real set
A is V16() real ext-real Element of REAL
1 / A is V16() real ext-real Element of REAL
[/(1 / A)\] is V16() real ext-real integer set
[/(1 / A)\] + 1 is V16() real ext-real integer Element of REAL
r1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
(r1 + 1) * A is V16() real ext-real Element of REAL
1 / (r1 + 1) is V16() real ext-real non negative Element of REAL
X is V16() real ext-real set
S is V16() real ext-real set
X - S is V16() real ext-real set
f is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (f + 1) is V16() real ext-real non negative Element of REAL
S + (1 / (f + 1)) is V16() real ext-real Element of REAL
X - (1 / (f + 1)) is V16() real ext-real Element of REAL
X is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
f is V16() real ext-real Element of REAL
R_EAL f is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
f is V16() real ext-real Element of REAL
R_EAL f is ext-real Element of ExtREAL
X is Relation-like Function-like ext-real-valued set
dom X is set
S is ext-real set
f is set
A is set
X . A is ext-real Element of ExtREAL
r is set
X . r is ext-real Element of ExtREAL
f is set
A is set
X . A is ext-real Element of ExtREAL
r is set
X . r is ext-real Element of ExtREAL
f is set
A is set
X . A is ext-real Element of ExtREAL
r is set
X . r is ext-real Element of ExtREAL
f is set
A is set
X . A is ext-real Element of ExtREAL
r is set
X . r is ext-real Element of ExtREAL
Coim (X,S) is set
{S} is non empty trivial 1 -element V60() set
X " {S} is set
f is set
A is set
X . A is ext-real Element of ExtREAL
A is set
X . A is ext-real Element of ExtREAL
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is ext-real set
(S,f) is set
bool X is non empty set
A is set
dom S is set
(S,f) is set
A is set
dom S is set
(S,f) is set
A is set
dom S is set
(S,f) is set
A is set
dom S is set
Coim (S,f) is set
{f} is non empty trivial 1 -element V60() set
S " {f} is set
Coim (S,f) is Element of bool X
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom S is set
f is set
A is ext-real Element of ExtREAL
(X,S,A) is Element of bool X
bool X is non empty set
f /\ (X,S,A) is Element of bool X
(X,S,A) is Element of bool X
f /\ (X,S,A) is Element of bool X
f \ (f /\ (X,S,A)) is Element of bool f
bool f is non empty set
r is set
S . r is ext-real Element of ExtREAL
r is set
r1 is Element of X
S . r1 is ext-real Element of ExtREAL
x1 is ext-real Element of ExtREAL
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom S is set
f is set
A is ext-real Element of ExtREAL
(X,S,A) is Element of bool X
bool X is non empty set
f /\ (X,S,A) is Element of bool X
(X,S,A) is Element of bool X
f /\ (X,S,A) is Element of bool X
f \ (f /\ (X,S,A)) is Element of bool f
bool f is non empty set
r is set
S . r is ext-real Element of ExtREAL
r is set
r1 is Element of X
S . r1 is ext-real Element of ExtREAL
x1 is ext-real Element of ExtREAL
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom S is set
f is set
A is ext-real Element of ExtREAL
(X,S,A) is Element of bool X
bool X is non empty set
f /\ (X,S,A) is Element of bool X
(X,S,A) is Element of bool X
f /\ (X,S,A) is Element of bool X
f \ (f /\ (X,S,A)) is Element of bool f
bool f is non empty set
r is set
S . r is ext-real Element of ExtREAL
r is set
r1 is Element of X
S . r1 is ext-real Element of ExtREAL
x1 is ext-real Element of ExtREAL
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom S is set
f is set
A is ext-real Element of ExtREAL
(X,S,A) is Element of bool X
bool X is non empty set
f /\ (X,S,A) is Element of bool X
(X,S,A) is Element of bool X
f /\ (X,S,A) is Element of bool X
f \ (f /\ (X,S,A)) is Element of bool f
bool f is non empty set
r is set
S . r is ext-real Element of ExtREAL
r is set
r1 is Element of X
S . r1 is ext-real Element of ExtREAL
x1 is ext-real Element of ExtREAL
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is set
A is ext-real Element of ExtREAL
(X,S,A) is Element of bool X
bool X is non empty set
{A} is non empty trivial 1 -element V60() set
S " {A} is set
f /\ (X,S,A) is Element of bool X
(X,S,A) is Element of bool X
f /\ (X,S,A) is Element of bool X
(X,S,A) is Element of bool X
(f /\ (X,S,A)) /\ (X,S,A) is Element of bool X
r is set
S . r is ext-real Element of ExtREAL
r1 is Element of X
dom S is set
r is set
S . r is ext-real Element of ExtREAL
r1 is Element of X
dom S is set
S . r1 is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
f is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng f is non empty countable M17(X,S)
meet (rng f) is Element of S
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
r is set
r1 is V16() real ext-real Element of REAL
R_EAL r1 is ext-real Element of ExtREAL
(X,A,(R_EAL r1)) is Element of bool X
r /\ (X,A,(R_EAL r1)) is Element of bool X
x1 is set
y is set
dom f is set
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . x is Element of S
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (x + 1))) is ext-real Element of ExtREAL
(X,A,(R_EAL (r1 - (1 / (x + 1))))) is Element of bool X
r /\ (X,A,(R_EAL (r1 - (1 / (x + 1))))) is Element of bool X
dom A is set
c₁₀ is Element of X
A . c₁₀ is ext-real Element of ExtREAL
(x + 1) " is non empty V16() real ext-real positive non negative Element of REAL
r1 + (1 / (x + 1)) is V16() real ext-real Element of REAL
x1 is set
dom A is set
A . x1 is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (y + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (y + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (y + 1))) is ext-real Element of ExtREAL
dom f is set
f . y is Element of S
(X,A,(R_EAL (r1 - (1 / (y + 1))))) is Element of bool X
r /\ (X,A,(R_EAL (r1 - (1 / (y + 1))))) is Element of bool X
dom f is set
f . 1 is Element of S
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (1 + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (1 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (1 + 1))) is ext-real Element of ExtREAL
(X,A,(R_EAL (r1 - (1 / (1 + 1))))) is Element of bool X
r /\ (X,A,(R_EAL (r1 - (1 / (1 + 1))))) is Element of bool X
y is ext-real Element of ExtREAL
c₁₀ is V16() real ext-real Element of REAL
c₁₁ is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
c₁₁ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (c₁₁ + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (c₁₁ + 1)) is V16() real ext-real Element of REAL
R_EAL c₁₀ is ext-real Element of ExtREAL
R_EAL (r1 - (1 / (c₁₁ + 1))) is ext-real Element of ExtREAL
x is Element of X
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,f:] is non empty V35() set
bool [:NAT,f:] is non empty V35() set
A is Relation-like NAT -defined f -valued Function-like quasi_total Element of bool [:NAT,f:]
rng A is non empty countable M17(X,f)
meet (rng A) is Element of f
r is set
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,S,(R_EAL r1)) is Element of bool X
r /\ (X,S,(R_EAL r1)) is Element of bool X
x1 is set
y is set
dom A is set
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
A . x is Element of f
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (x + 1))) is ext-real Element of ExtREAL
(X,S,(R_EAL (r1 + (1 / (x + 1))))) is Element of bool X
r /\ (X,S,(R_EAL (r1 + (1 / (x + 1))))) is Element of bool X
dom S is set
c₁₀ is Element of X
S . c₁₀ is ext-real Element of ExtREAL
(x + 1) " is non empty V16() real ext-real positive non negative Element of REAL
x1 is set
dom S is set
S . x1 is ext-real Element of ExtREAL
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (y + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (y + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (y + 1))) is ext-real Element of ExtREAL
dom A is set
A . y is Element of f
(X,S,(R_EAL (r1 + (1 / (y + 1))))) is Element of bool X
r /\ (X,S,(R_EAL (r1 + (1 / (y + 1))))) is Element of bool X
dom A is set
A . 1 is Element of f
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (1 + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (1 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (1 + 1))) is ext-real Element of ExtREAL
(X,S,(R_EAL (r1 + (1 / (1 + 1))))) is Element of bool X
r /\ (X,S,(R_EAL (r1 + (1 / (1 + 1))))) is Element of bool X
y is ext-real Element of ExtREAL
c₁₀ is V16() real ext-real Element of REAL
c₁₁ is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
c₁₁ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (c₁₁ + 1) is V16() real ext-real non negative Element of REAL
c₁₀ - (1 / (c₁₁ + 1)) is V16() real ext-real Element of REAL
r1 + (1 / (c₁₁ + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (c₁₁ + 1))) is ext-real Element of ExtREAL
R_EAL c₁₀ is ext-real Element of ExtREAL
x is Element of X
X is set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
f is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,f:] is non empty V35() set
bool [:NAT,f:] is non empty V35() set
A is Relation-like NAT -defined f -valued Function-like quasi_total Element of bool [:NAT,f:]
rng A is non empty countable M17(X,f)
union (rng A) is Element of f
r is set
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,S,(R_EAL r1)) is Element of bool X
r /\ (X,S,(R_EAL r1)) is Element of bool X
x1 is set
y is Element of X
dom S is set
S . y is ext-real Element of ExtREAL
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (1 + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (1 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (1 + 1))) is ext-real Element of ExtREAL
x is V16() real ext-real Element of REAL
r1 - x is V16() real ext-real Element of REAL
c₁₀ is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
c₁₀ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (c₁₀ + 1) is V16() real ext-real non negative Element of REAL
x + (1 / (c₁₀ + 1)) is V16() real ext-real Element of REAL
r1 - (1 / (c₁₀ + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (c₁₀ + 1))) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (x + 1))) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (x + 1))) is ext-real Element of ExtREAL
(X,S,(R_EAL (r1 - (1 / (x + 1))))) is Element of bool X
r /\ (X,S,(R_EAL (r1 - (1 / (x + 1))))) is Element of bool X
dom A is set
A . x is Element of f
y is set
x1 is set
y is set
dom A is set
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
A . x is Element of f
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (x + 1))) is ext-real Element of ExtREAL
(X,S,(R_EAL (r1 - (1 / (x + 1))))) is Element of bool X
r /\ (X,S,(R_EAL (r1 - (1 / (x + 1))))) is Element of bool X
dom S is set
S . x1 is ext-real Element of ExtREAL
c₁₀ is Element of X
S . c₁₀ is ext-real Element of ExtREAL
r1 + (1 / (x + 1)) is V16() real ext-real Element of REAL
X is set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
f is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng f is non empty countable M17(X,S)
union (rng f) is Element of S
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
r is set
r1 is V16() real ext-real Element of REAL
R_EAL r1 is ext-real Element of ExtREAL
(X,A,(R_EAL r1)) is Element of bool X
r /\ (X,A,(R_EAL r1)) is Element of bool X
x1 is set
y is Element of X
dom A is set
A . y is ext-real Element of ExtREAL
1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (1 + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (1 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (1 + 1))) is ext-real Element of ExtREAL
x is V16() real ext-real Element of REAL
x - r1 is V16() real ext-real Element of REAL
c₁₀ is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
c₁₀ + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (c₁₀ + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (c₁₀ + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (c₁₀ + 1))) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (x + 1))) is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (x + 1))) is ext-real Element of ExtREAL
(X,A,(R_EAL (r1 + (1 / (x + 1))))) is Element of bool X
r /\ (X,A,(R_EAL (r1 + (1 / (x + 1))))) is Element of bool X
dom f is set
f . x is Element of S
y is set
x1 is set
y is set
dom f is set
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . x is Element of S
x + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (x + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (x + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (x + 1))) is ext-real Element of ExtREAL
(X,A,(R_EAL (r1 + (1 / (x + 1))))) is Element of bool X
r /\ (X,A,(R_EAL (r1 + (1 / (x + 1))))) is Element of bool X
dom A is set
A . x1 is ext-real Element of ExtREAL
c₁₀ is Element of X
A . c₁₀ is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
f is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng f is non empty countable M17(X,S)
meet (rng f) is Element of S
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,A,+infty) is Element of bool X
A " {+infty} is set
r is set
r /\ (X,A,+infty) is Element of bool X
r1 is set
x1 is set
dom f is set
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . y is Element of S
R_EAL y is ext-real Element of ExtREAL
(X,A,(R_EAL y)) is Element of bool X
r /\ (X,A,(R_EAL y)) is Element of bool X
x is Element of X
A . x is ext-real Element of ExtREAL
dom A is set
r1 is set
dom A is set
A . r1 is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is set
f . x1 is Element of S
R_EAL x1 is ext-real Element of ExtREAL
(X,A,(R_EAL x1)) is Element of bool X
r /\ (X,A,(R_EAL x1)) is Element of bool X
y is V16() real ext-real Element of REAL
R_EAL y is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . x is Element of S
R_EAL x is ext-real Element of ExtREAL
(X,A,(R_EAL x)) is Element of bool X
r /\ (X,A,(R_EAL x)) is Element of bool X
dom f is set
f . 1 is Element of S
R_EAL 1 is ext-real Element of ExtREAL
(X,A,(R_EAL 1)) is Element of bool X
r /\ (X,A,(R_EAL 1)) is Element of bool X
x1 is Element of X
y is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
f is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng f is non empty countable M17(X,S)
union (rng f) is Element of S
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,A,+infty) is Element of bool X
r is set
r /\ (X,A,+infty) is Element of bool X
r1 is set
dom A is set
A . r1 is ext-real Element of ExtREAL
R_EAL 0 is ext-real Element of ExtREAL
x1 is V16() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
R_EAL x is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
R_EAL x1 is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
R_EAL x1 is ext-real Element of ExtREAL
y is Element of X
(X,A,(R_EAL x1)) is Element of bool X
r /\ (X,A,(R_EAL x1)) is Element of bool X
f . x1 is Element of S
dom f is set
r1 is set
x1 is set
dom f is set
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . y is Element of S
R_EAL y is ext-real Element of ExtREAL
(X,A,(R_EAL y)) is Element of bool X
r /\ (X,A,(R_EAL y)) is Element of bool X
dom A is set
A . r1 is ext-real Element of ExtREAL
x is Element of X
A . x is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
f is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng f is non empty countable M17(X,S)
meet (rng f) is Element of S
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,A,-infty) is Element of bool X
A " {-infty} is set
r is set
r /\ (X,A,-infty) is Element of bool X
r1 is set
x1 is set
dom f is set
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . y is Element of S
- y is V16() real ext-real non positive integer Element of REAL
R_EAL (- y) is ext-real Element of ExtREAL
(X,A,(R_EAL (- y))) is Element of bool X
r /\ (X,A,(R_EAL (- y))) is Element of bool X
x is Element of X
A . x is ext-real Element of ExtREAL
dom A is set
r1 is set
dom A is set
A . r1 is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
dom f is set
f . x1 is Element of S
- x1 is V16() real ext-real non positive integer Element of REAL
R_EAL (- x1) is ext-real Element of ExtREAL
(X,A,(R_EAL (- x1))) is Element of bool X
r /\ (X,A,(R_EAL (- x1))) is Element of bool X
y is V16() real ext-real Element of REAL
R_EAL y is ext-real Element of ExtREAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- x is V16() real ext-real non positive integer Element of REAL
f . x is Element of S
R_EAL (- x) is ext-real Element of ExtREAL
(X,A,(R_EAL (- x))) is Element of bool X
r /\ (X,A,(R_EAL (- x))) is Element of bool X
dom f is set
f . 1 is Element of S
- 1 is V16() real ext-real non positive integer Element of REAL
R_EAL (- 1) is ext-real Element of ExtREAL
(X,A,(R_EAL (- 1))) is Element of bool X
r /\ (X,A,(R_EAL (- 1))) is Element of bool X
x1 is Element of X
y is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
f is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng f is non empty countable M17(X,S)
union (rng f) is Element of S
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,A,-infty) is Element of bool X
r is set
r /\ (X,A,-infty) is Element of bool X
r1 is set
dom A is set
A . r1 is ext-real Element of ExtREAL
R_EAL (- 0) is ext-real Element of ExtREAL
x1 is V16() real ext-real Element of REAL
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- y is V16() real ext-real non positive integer Element of REAL
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- (y + 1) is V16() real ext-real non positive integer Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- x is V16() real ext-real non positive integer Element of REAL
R_EAL (- x) is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- x1 is V16() real ext-real non positive integer Element of REAL
R_EAL (- x1) is ext-real Element of ExtREAL
x1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- x1 is V16() real ext-real non positive integer Element of REAL
R_EAL (- x1) is ext-real Element of ExtREAL
y is Element of X
(X,A,(R_EAL (- x1))) is Element of bool X
r /\ (X,A,(R_EAL (- x1))) is Element of bool X
f . x1 is Element of S
dom f is set
r1 is set
x1 is set
dom f is set
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
f . y is Element of S
- y is V16() real ext-real non positive integer Element of REAL
R_EAL (- y) is ext-real Element of ExtREAL
(X,A,(R_EAL (- y))) is Element of bool X
r /\ (X,A,(R_EAL (- y))) is Element of bool X
dom A is set
A . r1 is ext-real Element of ExtREAL
x is Element of X
A . x is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
A is Element of S
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
A \ (A /\ (X,f,(R_EAL r))) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
A \ (A /\ (X,f,(R_EAL r))) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
A /\ (X,f,(R_EAL r1)) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
A is Element of S
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (r1 + 1) is V16() real ext-real non negative Element of REAL
r + (1 / (r1 + 1)) is V16() real ext-real Element of REAL
R_EAL (r + (1 / (r1 + 1))) is ext-real Element of ExtREAL
(X,f,(R_EAL (r + (1 / (r1 + 1))))) is Element of bool X
A /\ (X,f,(R_EAL (r + (1 / (r1 + 1))))) is Element of bool X
x1 is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
r1 is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng r1 is non empty countable M17(X,S)
meet (rng r1) is Element of S
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
r1 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (r1 + 1) is V16() real ext-real non negative Element of REAL
r - (1 / (r1 + 1)) is V16() real ext-real Element of REAL
R_EAL (r - (1 / (r1 + 1))) is ext-real Element of ExtREAL
(X,f,(R_EAL (r - (1 / (r1 + 1))))) is Element of bool X
A /\ (X,f,(R_EAL (r - (1 / (r1 + 1))))) is Element of bool X
x1 is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
r1 is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng r1 is non empty countable M17(X,S)
union (rng r1) is Element of S
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
A /\ (X,f,(R_EAL r1)) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
A is Element of S
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
A \ (A /\ (X,f,(R_EAL r))) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
A \ (A /\ (X,f,(R_EAL r))) is Element of bool X
r is V16() real ext-real set
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
A /\ (X,f,(R_EAL r1)) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
A is Element of S
r is Element of S
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
r /\ (X,f,(R_EAL r1)) is Element of bool X
A /\ (X,f,(R_EAL r1)) is Element of bool X
r /\ (A /\ (X,f,(R_EAL r1))) is Element of bool X
r /\ A is M7(X,S)
(r /\ A) /\ (X,f,(R_EAL r1)) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
A is Element of S
r is Element of S
A \/ r is M7(X,S)
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
(A \/ r) /\ (X,f,(R_EAL r1)) is Element of bool X
A /\ (X,f,(R_EAL r1)) is Element of bool X
r /\ (X,f,(R_EAL r1)) is Element of bool X
(A /\ (X,f,(R_EAL r1))) \/ (r /\ (X,f,(R_EAL r1))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
A is Element of S
r is V16() real ext-real Element of REAL
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is V16() real ext-real Element of REAL
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
(A /\ (X,f,(R_EAL r))) /\ (X,f,(R_EAL r1)) is Element of bool X
A /\ (X,f,(R_EAL r1)) is Element of bool X
x1 is V16() real ext-real Element of REAL
R_EAL x1 is ext-real Element of ExtREAL
(X,f,(R_EAL x1)) is Element of bool X
A /\ (X,f,(R_EAL x1)) is Element of bool X
(X,f,(R_EAL x1)) is Element of bool X
A /\ (X,f,(R_EAL x1)) is Element of bool X
A \ (A /\ (X,f,(R_EAL x1))) is Element of bool X
x1 is V16() real ext-real Element of REAL
R_EAL x1 is ext-real Element of ExtREAL
(X,f,(R_EAL x1)) is Element of bool X
A /\ (X,f,(R_EAL x1)) is Element of bool X
y is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
y + 1 is epsilon-transitive epsilon-connected ordinal natural non empty V16() real ext-real positive non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
1 / (y + 1) is V16() real ext-real non negative Element of REAL
x1 + (1 / (y + 1)) is V16() real ext-real Element of REAL
R_EAL (x1 + (1 / (y + 1))) is ext-real Element of ExtREAL
(X,f,(R_EAL (x1 + (1 / (y + 1))))) is Element of bool X
A /\ (X,f,(R_EAL (x1 + (1 / (y + 1))))) is Element of bool X
x is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
y is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng y is non empty countable M17(X,S)
union (rng y) is Element of S
(A /\ (X,f,(R_EAL r))) /\ (A /\ (X,f,(R_EAL r1))) is Element of bool X
(A /\ (X,f,(R_EAL r))) /\ A is Element of bool X
((A /\ (X,f,(R_EAL r))) /\ A) /\ (X,f,(R_EAL r1)) is Element of bool X
A /\ A is M7(X,S)
(X,f,(R_EAL r)) /\ (A /\ A) is Element of bool X
((X,f,(R_EAL r)) /\ (A /\ A)) /\ (X,f,(R_EAL r1)) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
(X,f,+infty) is Element of bool X
f " {+infty} is set
A is Element of S
A /\ (X,f,+infty) is Element of bool X
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
r is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng r is non empty countable M17(X,S)
meet (rng r) is Element of S
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
(X,f,-infty) is Element of bool X
f " {-infty} is set
A is Element of S
A /\ (X,f,-infty) is Element of bool X
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- r is V16() real ext-real non positive integer Element of REAL
R_EAL (- r) is ext-real Element of ExtREAL
(X,f,(R_EAL (- r))) is Element of bool X
A /\ (X,f,(R_EAL (- r))) is Element of bool X
r1 is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
r is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng r is non empty countable M17(X,S)
meet (rng r) is Element of S
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
(X,f,-infty) is Element of bool X
(X,f,+infty) is Element of bool X
A is Element of S
A /\ (X,f,-infty) is Element of bool X
(A /\ (X,f,-infty)) /\ (X,f,+infty) is Element of bool X
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
- r is V16() real ext-real non positive integer Element of REAL
R_EAL (- r) is ext-real Element of ExtREAL
(X,f,(R_EAL (- r))) is Element of bool X
A /\ (X,f,(R_EAL (- r))) is Element of bool X
r1 is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
r is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng r is non empty countable M17(X,S)
union (rng r) is Element of S
A /\ (X,f,+infty) is Element of bool X
r is epsilon-transitive epsilon-connected ordinal natural V16() real ext-real non negative integer rational V35() cardinal V59() V60() V61() V62() V63() V64() Element of NAT
R_EAL r is ext-real Element of ExtREAL
(X,f,(R_EAL r)) is Element of bool X
A /\ (X,f,(R_EAL r)) is Element of bool X
r1 is Element of S
[:NAT,S:] is non empty V35() set
bool [:NAT,S:] is non empty V35() set
r is Relation-like NAT -defined S -valued Function-like quasi_total Element of bool [:NAT,S:]
rng r is non empty countable M17(X,S)
union (rng r) is Element of S
(A /\ (X,f,-infty)) /\ (A /\ (X,f,+infty)) is Element of bool X
(A /\ (X,f,-infty)) /\ A is Element of bool X
((A /\ (X,f,-infty)) /\ A) /\ (X,f,+infty) is Element of bool X
A /\ A is M7(X,S)
(X,f,-infty) /\ (A /\ A) is Element of bool X
((X,f,-infty) /\ (A /\ A)) /\ (X,f,+infty) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom A is set
r is Element of S
r1 is V16() real ext-real Element of REAL
R_EAL r1 is ext-real Element of ExtREAL
(X,f,(R_EAL r1)) is Element of bool X
r /\ (X,f,(R_EAL r1)) is Element of bool X
(X,A,(R_EAL r1)) is Element of bool X
(r /\ (X,f,(R_EAL r1))) /\ (X,A,(R_EAL r1)) is Element of bool X
r /\ (X,A,(R_EAL r1)) is Element of bool X
(r /\ (X,f,(R_EAL r1))) /\ (r /\ (X,A,(R_EAL r1))) is Element of bool X
(r /\ (X,f,(R_EAL r1))) /\ r is Element of bool X
((r /\ (X,f,(R_EAL r1))) /\ r) /\ (X,A,(R_EAL r1)) is Element of bool X
r /\ r is M7(X,S)
(r /\ r) /\ (X,f,(R_EAL r1)) is Element of bool X
((r /\ r) /\ (X,f,(R_EAL r1))) /\ (X,A,(R_EAL r1)) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)
f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
dom f is set
A is Element of S
r is V16() real ext-real Element of REAL
(X,f,r) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of bool [:X,ExtREAL:]
r1 is V16() real ext-real set
R_EAL r1 is ext-real Element of ExtREAL
(X,(X,f,r),(R_EAL r1)) is Element of bool X
A /\ (X,(X,f,r),(R_EAL r1)) is Element of bool X
r1 / r is V16() real ext-real Element of REAL
x1 is V16() real ext-real Element of REAL
r * x1 is V16() real ext-real Element of REAL
R_EAL x1 is ext-real Element of ExtREAL
(X,f,(R_EAL x1)) is Element of bool X
y is Element of X
dom (X,f,r) is set
f . y is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r1) / (R_EAL r) is ext-real Element of ExtREAL
((R_EAL r1) / (R_EAL r)) * (R_EAL r) is ext-real Element of ExtREAL
(f . y) * (R_EAL r) is ext-real Element of ExtREAL
(r1 / r) * r is V16() real ext-real Element of REAL
r / r is V16() real ext-real Element of REAL
r1 / (r / r) is V16() real ext-real Element of REAL
r1 / 1 is V16() real ext-real Element of REAL
(X,f,r) . y is ext-real Element of ExtREAL
(R_EAL r) * (f . y) is ext-real Element of ExtREAL
y is Element of X
dom (X,f,r) is set
(X,f,r) . y is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r) * (R_EAL x1) is ext-real Element of ExtREAL
((R_EAL r) * (R_EAL x1)) / (R_EAL r) is ext-real Element of ExtREAL
((X,f,r) . y) / (R_EAL r) is ext-real Element of ExtREAL
(r * x1) / r is V16() real ext-real Element of REAL
r / r is V16() real ext-real Element of REAL
x1 / (r / r) is V16() real ext-real Element of REAL
x1 / 1 is V16() real ext-real Element of REAL
f . y is ext-real Element of ExtREAL
R_EAL x1 is ext-real Element of ExtREAL
(X,f,(R_EAL x1)) is Element of bool X
y is Element of X
dom (X,f,r) is set
f . y is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r1) / (R_EAL r) is ext-real Element of ExtREAL
((R_EAL r1) / (R_EAL r)) * (R_EAL r) is ext-real Element of ExtREAL
(f . y) * (R_EAL r) is ext-real Element of ExtREAL
(r1 / r) * r is V16() real ext-real Element of REAL
r / r is V16() real ext-real Element of REAL
r1 / (r / r) is V16() real ext-real Element of REAL
r1 / 1 is V16() real ext-real Element of REAL
(X,f,r) . y is ext-real Element of ExtREAL
(R_EAL r) * (f . y) is ext-real Element of ExtREAL
y is Element of X
dom (X,f,r) is set
(X,f,r) . y is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r) * (R_EAL x1) is ext-real Element of ExtREAL
((X,f,r) . y) / (R_EAL r) is ext-real Element of ExtREAL
((R_EAL r) * (R_EAL x1)) / (R_EAL r) is ext-real Element of ExtREAL
(r * x1) / r is V16() real ext-real Element of REAL
r / r is V16() real ext-real Element of REAL
x1 / (r / r) is V16() real ext-real Element of REAL
x1 / 1 is V16() real ext-real Element of REAL
f . y is ext-real Element of ExtREAL
x1 is set
y is Element of X
dom (X,f,r) is set
(X,f,r) . y is ext-real Element of ExtREAL
x is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
f . y is ext-real Element of ExtREAL
(R_EAL r) * (f . y) is ext-real Element of ExtREAL
x1 is Element of X
dom (X,f,r) is set
(X,f,r) . x1 is ext-real Element of ExtREAL
rng (X,f,r) is V60() set
y is ext-real Element of ExtREAL
x is Element of X
(X,f,r) . x is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
f . x is ext-real Element of ExtREAL
(R_EAL r) * (f . x) is ext-real Element of ExtREAL