:: MESFUNC1 semantic presentation

REAL is non empty V35() V59() V60() V61() V65() set

bool REAL is non empty V35() set
ExtREAL is non empty V60() set
is non empty V35() ext-real-valued set
bool is non empty V35() set
bool ExtREAL is non empty set

bool omega is non empty V35() set

bool is non empty V35() set
bool () 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
is non empty V35() complex-valued set
bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() set

bool is non empty V35() 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

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

() is V59() V60() V61() Element of bool REAL

bool [:NAT,():] is non empty V35() set

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

X . A is V16() real ext-real Element of ExtREAL

X . r is V16() real ext-real Element of ExtREAL

- (- 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

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

X is set

bool RAT is non empty V35() set

S is V59() V60() V61() V62() Element of bool RAT
f is rational set

r / X is V16() real ext-real set

r / X is V16() real ext-real set

r1 / X is V16() real ext-real set
f is rational set
A is rational 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

r is rational set

r1 / X is V16() real ext-real set
r is rational set

r1 / X is V16() real ext-real set

((X + 1)) is V59() V60() V61() V62() Element of bool RAT

0 / S is V16() real ext-real Element of REAL
f is rational set

((X + 1)) is non empty V59() V60() V61() V62() Element of bool RAT

S / (X + 1) is V16() real ext-real Element of REAL

f / A is V16() real ext-real set
r1 is rational set

bool [:INT,((X + 1)):] is non empty V35() set

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

S . r is V16() real ext-real Element of ExtREAL
r / (X + 1) is V16() real ext-real Element of REAL

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 / (X + 1) is V16() real ext-real Element of REAL

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 + 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,():] is non empty V35() set
bool [:NAT,():] is non empty V35() set

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 + 1)) is non empty V59() V60() V61() V62() Element of bool RAT
S is set
dom X is set
f is rational set

() - 1 is V16() real ext-real integer Element of REAL

() / (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 + 1)) is non empty V59() V60() V61() V62() Element of bool RAT

X is non empty set

is non empty ext-real-valued set
bool 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
is non empty trivial 1 -element V60() set
S " is set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
is non empty trivial 1 -element V60() set
f " is set
() /\ () is set
S " is set
f " is set
() /\ () is set
(() /\ ()) \/ (() /\ ()) is set
((dom S) /\ (dom f)) \ ((() /\ ()) \/ (() /\ ())) is Element of bool ((dom S) /\ (dom f))
bool ((dom S) /\ (dom f)) is non empty set

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

dom A is set

dom r is set

dom r1 is set
(dom r) /\ (dom r1) is set
r " is set
r1 " is set
() /\ () is set
r " is set
r1 " is set
() /\ () is set
(() /\ ()) \/ (() /\ ()) is set
((dom r) /\ (dom r1)) \ ((() /\ ()) \/ (() /\ ())) is Element of bool ((dom r) /\ (dom r1))
bool ((dom r) /\ (dom r1)) is non empty set
(dom r1) /\ (dom r) is set
() /\ () is set
() /\ () is set
(() /\ ()) \/ (() /\ ()) is set
((dom r1) /\ (dom r)) \ ((() /\ ()) \/ (() /\ ())) 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
() /\ () is set
() /\ () is set
(() /\ ()) \/ (() /\ ()) is set
((dom S) /\ (dom f)) \ ((() /\ ()) \/ (() /\ ())) is Element of bool ((dom S) /\ (dom f))

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

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

dom A is set

dom r is 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

is non empty ext-real-valued set
bool is non empty set
dom S is set

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
() * (S . r) is ext-real Element of ExtREAL
X is non empty set
is non empty ext-real-valued set
bool is non empty set

f is V16() real ext-real Element of REAL

dom (X,S,f) is set

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) / () is ext-real Element of ExtREAL
() * (S . A) is ext-real 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

is non empty ext-real-valued set
bool is non empty set
dom S is set

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

is non empty ext-real-valued set
bool is non empty set
dom S is set

is non empty trivial 1 -element V59() V60() V61() V62() V63() V64() set
S " is set
(dom S) \ () is Element of bool (dom S)
bool (dom S) is non empty set

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
() / (S . r) is ext-real Element of ExtREAL
X is non empty set
is non empty ext-real-valued set
bool is non empty set

dom (X,S,1) is set
dom S is set
S " is set
(dom S) \ () 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

() / (S . f) is ext-real Element of ExtREAL
X is non empty set

is non empty ext-real-valued set
bool is non empty set
dom S is set

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 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 + 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

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

f is V16() real ext-real Element of REAL

f is V16() real ext-real Element of REAL

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

bool is non empty set

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

bool is non empty set

dom S is set
f is set

(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

bool is non empty set

dom S is set
f is set

(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

bool is non empty set

dom S is set
f is set

(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

bool is non empty set

dom S is set
f is set

(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

bool is non empty set

f is set

(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

bool 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

rng f is non empty countable M17(X,S)
meet (rng f) is Element of S

r is set
r1 is V16() real ext-real Element of REAL

(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

f . x is Element of S

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
c10 is Element of X
A . c10 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

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 + 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

c10 is V16() real ext-real Element of REAL

1 / (c11 + 1) is V16() real ext-real non negative Element of REAL
r1 - (1 / (c11 + 1)) is V16() real ext-real Element of REAL
R_EAL c10 is ext-real Element of ExtREAL
R_EAL (r1 - (1 / (c11 + 1))) is ext-real Element of ExtREAL
x is Element of X
X is set

bool is non empty set
bool X is non empty set
bool (bool X) is non empty set

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

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

(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

A . x is Element of f

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
c10 is Element of X
S . c10 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

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 + 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

c10 is V16() real ext-real Element of REAL

1 / (c11 + 1) is V16() real ext-real non negative Element of REAL
c10 - (1 / (c11 + 1)) is V16() real ext-real Element of REAL
r1 + (1 / (c11 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (c11 + 1))) is ext-real Element of ExtREAL
R_EAL c10 is ext-real Element of ExtREAL
x is Element of X
X is set

bool is non empty set
bool X is non empty set
bool (bool X) is non empty set

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

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

(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 + 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

1 / (c10 + 1) is V16() real ext-real non negative Element of REAL
x + (1 / (c10 + 1)) is V16() real ext-real Element of REAL
r1 - (1 / (c10 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 - (1 / (c10 + 1))) is ext-real Element of ExtREAL

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

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

A . x is Element of f

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
c10 is Element of X
S . c10 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

bool 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

rng f is non empty countable M17(X,S)
union (rng f) is Element of S

r is set
r1 is V16() real ext-real Element of REAL

(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 + 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

1 / (c10 + 1) is V16() real ext-real non negative Element of REAL
r1 + (1 / (c10 + 1)) is V16() real ext-real Element of REAL
R_EAL (r1 + (1 / (c10 + 1))) is ext-real Element of ExtREAL

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

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

f . x is Element of S

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
c10 is Element of X
A . c10 is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set

bool 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

rng f is non empty countable M17(X,S)
meet (rng f) is Element of S

(X,A,+infty) is Element of bool X
A " is set
r is set
r /\ (X,A,+infty) is Element of bool X
r1 is set
x1 is set
dom f is set

f . y is Element of S

(X,A,()) is Element of bool X
r /\ (X,A,()) 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

dom f is set
f . x1 is Element of S

(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

f . x is Element of S

(X,A,()) is Element of bool X
r /\ (X,A,()) is Element of bool X
dom f is set
f . 1 is Element of S

(X,A,()) is Element of bool X
r /\ (X,A,()) is Element of bool X
x1 is Element of X

X is set
bool X is non empty set
bool (bool X) is non empty set

bool 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

rng f is non empty countable M17(X,S)
union (rng f) is Element of S

(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

x1 is V16() real ext-real Element of REAL

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

f . y is Element of S

(X,A,()) is Element of bool X
r /\ (X,A,()) 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

bool 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

rng f is non empty countable M17(X,S)
meet (rng f) is Element of S

(X,A,-infty) is Element of bool X
A " is set
r is set
r /\ (X,A,-infty) is Element of bool X
r1 is set
x1 is set
dom f is set

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

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

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

X is set
bool X is non empty set
bool (bool X) is non empty set

bool 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

rng f is non empty countable M17(X,S)
union (rng f) is Element of S

(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

x1 is V16() real ext-real Element of REAL

- (y + 1) is V16() real ext-real non positive integer Element of REAL

R_EAL (- x) is ext-real Element of ExtREAL

- x1 is V16() real ext-real non positive integer Element of REAL
R_EAL (- x1) is ext-real Element of ExtREAL

- 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

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 non empty set
bool X is non empty set
bool (bool X) is non empty set
is non empty ext-real-valued set
bool 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
is non empty ext-real-valued set
bool is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)

dom f is set
A is Element of S
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
A \ (A /\ (X,f,())) is Element of bool X
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
A \ (A /\ (X,f,())) is Element of bool X
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
r1 is V16() real ext-real set

(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
is non empty ext-real-valued set
bool is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() V91(X) Element of bool (bool X)

A is Element of S
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X

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

rng r1 is non empty countable M17(X,S)
meet (rng r1) is Element of S
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X
r is V16() real ext-real set

(X,f,()) is Element of bool X
A /\ (X,f,()) is Element of bool X

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