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

A . c

(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

c

c

1 / (c

r1 - (1 / (c

R_EAL c

R_EAL (r1 - (1 / (c

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

S . c

(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

c

c

1 / (c

c

r1 + (1 / (c

R_EAL (r1 + (1 / (c

R_EAL c

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

c

1 / (c

x + (1 / (c

r1 - (1 / (c

R_EAL (r1 - (1 / (c

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

S . c

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

c

1 / (c

r1 + (1 / (c

R_EAL (r1 + (1 / (c

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

A . c

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