REAL is non empty V35() V59() V60() V61() V65() set
NAT is V59() V60() V61() V62() V63() V64() V65() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V60() set
[:NAT,ExtREAL:] is V67() set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
COMPLEX is non empty V35() V59() V65() set
omega is V59() V60() V61() V62() V63() V64() V65() set
bool omega is non empty set
[:NAT,REAL:] is V66() V67() V68() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty 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 set
bool RAT is non empty set
[:COMPLEX,COMPLEX:] is non empty V66() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V66() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V66() V67() V68() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V66() V67() V68() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is non empty V11( RAT ) V66() V67() V68() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is non empty V11( RAT ) V66() V67() V68() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is non empty V11( RAT ) V11( INT ) V66() V67() V68() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is non empty V11( RAT ) V11( INT ) V66() V67() V68() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is V11( RAT ) V11( INT ) V66() V67() V68() V69() set
[:[:NAT,NAT:],NAT:] is V11( RAT ) V11( INT ) V66() V67() V68() V69() set
bool [:[:NAT,NAT:],NAT:] is non empty set
K514() is set
1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
{} is empty V59() V60() V61() V62() V63() V64() V65() set
the empty V59() V60() V61() V62() V63() V64() V65() set is empty V59() V60() V61() V62() V63() V64() V65() set
{{},1} is non empty set
0. is empty ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL
0 is empty ordinal natural V24() real ext-real non positive non negative V29() V59() V60() V61() V62() V63() V64() V65() rational Element of NAT
-infty is non empty non real ext-real non positive negative Element of ExtREAL
{-infty} is non empty V60() set
+infty is non empty non real ext-real positive non negative Element of ExtREAL
{+infty} is non empty V60() set
Seg 1 is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b1 where b1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b1 & b1 <= 1 ) } is set
{1} is non empty V59() V60() V61() V62() V63() V64() set
2 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
Seg 2 is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b1 where b1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b1 & b1 <= 2 ) } is set
{1,2} is non empty V59() V60() V61() V62() V63() V64() set
- 1 is V24() real ext-real non positive rational Element of REAL
bool {} is non empty set
{{}} is non empty 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 non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
|.(R_EAL S).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
abs S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL (abs S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
M is Element of X
dom |.(R_EAL S).| is Element of bool X
bool X is non empty set
|.(R_EAL S).| . M is ext-real Element of ExtREAL
(R_EAL S) . M is ext-real Element of ExtREAL
|.((R_EAL S) . M).| is ext-real Element of ExtREAL
S . M is V24() real ext-real Element of REAL
abs (S . M) is V24() real ext-real Element of REAL
(R_EAL (abs S)) . M is ext-real Element of ExtREAL
dom (R_EAL S) is Element of bool X
dom (abs S) 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 V67() set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom f is Element of bool X
r is V24() real ext-real Element of REAL
B is Element of S
<*B*> is V7() V10( NAT ) V11(S) Function-like FinSequence-like FinSequence of S
[1,B] is set
{1,B} is non empty set
{{1,B},{1}} is non empty set
{[1,B]} is non empty set
dom <*B*> is V59() V60() V61() V62() V63() V64() Element of bool NAT
F is ordinal natural V24() real ext-real non negative set
n is ordinal natural V24() real ext-real non negative set
<*B*> . F is set
<*B*> . n is set
F is ordinal natural V24() real ext-real non negative set
<*B*> . F is set
F is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng F is Element of bool S
bool S is non empty set
union (rng F) is set
dom F is V59() V60() V61() V62() V63() V64() Element of bool NAT
F . 1 is set
<*(F . 1)*> is V7() Function-like set
[1,(F . 1)] is set
{1,(F . 1)} is non empty set
{{1,(F . 1)},{1}} is non empty set
{[1,(F . 1)]} is non empty set
{(F . 1)} is non empty set
n is ordinal natural V24() real ext-real non negative set
x is Element of X
F . n is set
y is Element of X
f . x is ext-real Element of ExtREAL
f . y is ext-real Element of ExtREAL
c7 is Element of X
f . c7 is ext-real Element of ExtREAL
- +infty is ext-real Element of ExtREAL
|.(f . c7).| is ext-real Element of ExtREAL
c7 is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng c7 is Element of bool S
bool S is non empty set
union (rng c7) is set
dom c7 is V59() V60() V61() V62() V63() V64() Element of bool NAT
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
M is V24() real ext-real set
less_dom (S,M) is set
f is set
S . f is V24() real ext-real Element of REAL
R_EAL M is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL
B is V24() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
M is V24() real ext-real set
less_eq_dom (S,M) is set
f is set
S . f is V24() real ext-real Element of REAL
R_EAL M is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL
B is V24() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
M is V24() real ext-real Element of REAL
great_dom (S,M) is set
f is set
S . f is V24() real ext-real Element of REAL
R_EAL M is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL
B is V24() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
M is V24() real ext-real Element of REAL
great_eq_dom (S,M) is set
f is set
S . f is V24() real ext-real Element of REAL
R_EAL M is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL
B is V24() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
M is V24() real ext-real Element of REAL
eq_dom (S,M) is set
f is set
S . f is V24() real ext-real Element of REAL
R_EAL M is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
r is V24() real ext-real Element of REAL
B is V24() real ext-real Element of REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is set
M is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,M:] is set
bool [:NAT,M:] is non empty set
f is V7() V10( NAT ) V11(M) Function-like V32( NAT ,M) Element of bool [:NAT,M:]
rng f is non empty Element of bool (bool X)
meet (rng f) is Element of bool X
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
B is V24() real ext-real Element of REAL
great_eq_dom (r,B) is set
S /\ (great_eq_dom (r,B)) is set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
c7 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c7 is set
c7 + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
1 / (c7 + 1) is V24() real ext-real non negative rational Element of COMPLEX
B - (1 / (c7 + 1)) is V24() real ext-real Element of REAL
R_EAL (B - (1 / (c7 + 1))) is ext-real Element of ExtREAL
great_dom ((R_EAL r),(R_EAL (B - (1 / (c7 + 1))))) is Element of bool X
S /\ (great_dom ((R_EAL r),(R_EAL (B - (1 / (c7 + 1)))))) is Element of bool X
R_EAL B is ext-real Element of ExtREAL
great_eq_dom (r,(R_EAL B)) is set
S /\ (great_eq_dom (r,(R_EAL B))) is set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is set
M is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,M:] is set
bool [:NAT,M:] is non empty set
f is V7() V10( NAT ) V11(M) Function-like V32( NAT ,M) Element of bool [:NAT,M:]
rng f is non empty Element of bool (bool X)
meet (rng f) is Element of bool X
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
B is V24() real ext-real Element of REAL
less_eq_dom (r,B) is set
S /\ (less_eq_dom (r,B)) is set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
c7 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c7 is set
c7 + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
1 / (c7 + 1) is V24() real ext-real non negative rational Element of COMPLEX
B + (1 / (c7 + 1)) is V24() real ext-real Element of REAL
R_EAL (B + (1 / (c7 + 1))) is ext-real Element of ExtREAL
less_dom ((R_EAL r),(R_EAL (B + (1 / (c7 + 1))))) is Element of bool X
S /\ (less_dom ((R_EAL r),(R_EAL (B + (1 / (c7 + 1)))))) is Element of bool X
R_EAL B is ext-real Element of ExtREAL
less_eq_dom (r,(R_EAL B)) is set
S /\ (less_eq_dom (r,(R_EAL B))) is set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is set
M is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,M:] is set
bool [:NAT,M:] is non empty set
f is V7() V10( NAT ) V11(M) Function-like V32( NAT ,M) Element of bool [:NAT,M:]
rng f is non empty Element of bool (bool X)
union (rng f) is Element of bool X
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
B is V24() real ext-real Element of REAL
less_dom (r,B) is set
S /\ (less_dom (r,B)) is set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
c7 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c7 is set
c7 + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
1 / (c7 + 1) is V24() real ext-real non negative rational Element of COMPLEX
B - (1 / (c7 + 1)) is V24() real ext-real Element of REAL
R_EAL (B - (1 / (c7 + 1))) is ext-real Element of ExtREAL
less_eq_dom ((R_EAL r),(R_EAL (B - (1 / (c7 + 1))))) is Element of bool X
S /\ (less_eq_dom ((R_EAL r),(R_EAL (B - (1 / (c7 + 1)))))) is Element of bool X
R_EAL B is ext-real Element of ExtREAL
less_dom (r,(R_EAL B)) is set
S /\ (less_dom (r,(R_EAL B))) is set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is set
M is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:NAT,M:] is set
bool [:NAT,M:] is non empty set
f is V7() V10( NAT ) V11(M) Function-like V32( NAT ,M) Element of bool [:NAT,M:]
rng f is non empty Element of bool (bool X)
union (rng f) is Element of bool X
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
B is V24() real ext-real Element of REAL
great_dom (r,B) is set
S /\ (great_dom (r,B)) is set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
c7 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c7 is set
c7 + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
1 / (c7 + 1) is V24() real ext-real non negative rational Element of COMPLEX
B + (1 / (c7 + 1)) is V24() real ext-real Element of REAL
R_EAL (B + (1 / (c7 + 1))) is ext-real Element of ExtREAL
great_eq_dom ((R_EAL r),(R_EAL (B + (1 / (c7 + 1))))) is Element of bool X
S /\ (great_eq_dom ((R_EAL r),(R_EAL (B + (1 / (c7 + 1)))))) is Element of bool X
R_EAL B is ext-real Element of ExtREAL
great_dom (r,(R_EAL B)) is set
S /\ (great_dom (r,(R_EAL B))) is set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is Element of S
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
r is V24() real ext-real set
less_dom (M,r) is set
f /\ (less_dom (M,r)) is Element of bool X
R_EAL r is ext-real Element of ExtREAL
r is V24() real ext-real set
R_EAL r is ext-real Element of ExtREAL
less_dom (M,(R_EAL r)) is set
f /\ (less_dom (M,(R_EAL r))) is Element of bool X
r is V24() real ext-real set
R_EAL r is ext-real Element of ExtREAL
less_dom (M,(R_EAL r)) is set
f /\ (less_dom (M,(R_EAL r))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
f is Element of S
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
r is V24() real ext-real set
great_eq_dom (M,r) is set
f /\ (great_eq_dom (M,r)) is Element of bool X
R_EAL r is ext-real Element of ExtREAL
great_eq_dom (M,(R_EAL r)) is set
f /\ (great_eq_dom (M,(R_EAL r))) is Element of bool X
r is V24() real ext-real set
R_EAL r is ext-real Element of ExtREAL
great_eq_dom (M,(R_EAL r)) is set
f /\ (great_eq_dom (M,(R_EAL r))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is Element of S
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
r is V24() real ext-real set
less_eq_dom (M,r) is set
f /\ (less_eq_dom (M,r)) is Element of bool X
R_EAL r is ext-real Element of ExtREAL
r is V24() real ext-real set
R_EAL r is ext-real Element of ExtREAL
less_eq_dom (M,(R_EAL r)) is set
f /\ (less_eq_dom (M,(R_EAL r))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
f is Element of S
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
r is V24() real ext-real set
great_dom (M,r) is set
f /\ (great_dom (M,r)) is Element of bool X
R_EAL r is ext-real Element of ExtREAL
great_dom (M,(R_EAL r)) is set
f /\ (great_dom (M,(R_EAL r))) is Element of bool X
r is V24() real ext-real set
R_EAL r is ext-real Element of ExtREAL
great_dom (M,(R_EAL r)) is set
f /\ (great_dom (M,(R_EAL r))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is Element of S
r is Element of S
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is Element of S
r is Element of S
f \/ r is M7(X,S)
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
f is Element of S
r is V24() real ext-real Element of REAL
great_dom (M,r) is set
f /\ (great_dom (M,r)) is Element of bool X
B is V24() real ext-real Element of REAL
less_dom (M,B) is set
(f /\ (great_dom (M,r))) /\ (less_dom (M,B)) is Element of bool X
R_EAL r is ext-real Element of ExtREAL
R_EAL B is ext-real Element of ExtREAL
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
r is Element of S
B is V24() real ext-real Element of REAL
less_dom (M,B) is set
r /\ (less_dom (M,B)) is Element of bool X
great_dom (f,B) is set
(r /\ (less_dom (M,B))) /\ (great_dom (f,B)) is Element of bool X
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL B is ext-real Element of ExtREAL
less_dom (M,(R_EAL B)) is set
r /\ (less_dom (M,(R_EAL B))) is Element of bool X
great_dom (f,(R_EAL B)) is set
(r /\ (less_dom (M,(R_EAL B)))) /\ (great_dom (f,(R_EAL B))) is Element of bool X
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
M is V24() real ext-real Element of REAL
M (#) S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL (M (#) S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
M (#) (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL (M (#) S)) is Element of bool X
bool X is non empty set
dom (R_EAL S) is Element of bool X
dom (M (#) (R_EAL S)) is Element of bool X
f is set
(R_EAL (M (#) S)) . f is ext-real Element of ExtREAL
S . f is V24() real ext-real Element of REAL
M * (S . f) is V24() real ext-real Element of REAL
R_EAL M is ext-real Element of ExtREAL
R_EAL (S . f) is ext-real Element of ExtREAL
(R_EAL M) * (R_EAL (S . f)) is ext-real Element of ExtREAL
(M (#) (R_EAL S)) . f 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,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
f is Element of S
r is V24() real ext-real Element of REAL
r (#) M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
r (#) (R_EAL M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (r (#) M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
dom (R_EAL S) is Element of bool X
bool X is non empty set
dom S is Element of bool X
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
S + M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL (S + M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL S) + (R_EAL M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
S - M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- M is V7() Function-like V66() set
- 1 is V24() real ext-real non positive rational set
(- 1) (#) M is V7() Function-like set
S + (- M) is V7() Function-like set
R_EAL (S - M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL S) - (R_EAL M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL (S + M)) is Element of bool X
dom (R_EAL M) is Element of bool X
(dom (R_EAL S)) /\ (dom (R_EAL M)) is Element of bool X
dom (R_EAL (S - M)) is Element of bool X
dom M is Element of bool X
(dom S) /\ (dom M) is Element of bool X
dom ((R_EAL S) - (R_EAL M)) is Element of bool X
dom (S - M) is Element of bool X
f is set
((R_EAL S) - (R_EAL M)) . f is ext-real Element of ExtREAL
(R_EAL S) . f is ext-real Element of ExtREAL
(R_EAL M) . f is ext-real Element of ExtREAL
((R_EAL S) . f) - ((R_EAL M) . f) is ext-real Element of ExtREAL
S . f is V24() real ext-real Element of REAL
M . f is V24() real ext-real Element of REAL
(S . f) - (M . f) is V24() real ext-real Element of REAL
(S - M) . f is V24() real ext-real Element of REAL
dom ((R_EAL S) + (R_EAL M)) is Element of bool X
dom (S + M) is Element of bool X
f is set
((R_EAL S) + (R_EAL M)) . f is ext-real Element of ExtREAL
(R_EAL S) . f is ext-real Element of ExtREAL
(R_EAL M) . f is ext-real Element of ExtREAL
((R_EAL S) . f) + ((R_EAL M) . f) is ext-real Element of ExtREAL
S . f is V24() real ext-real Element of REAL
M . f is V24() real ext-real Element of REAL
(S . f) + (M . f) is V24() real ext-real Element of REAL
(S + M) . f is V24() real ext-real Element of REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:RAT,S:] is non empty set
bool [:RAT,S:] is non empty set
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M + f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
B is V24() real ext-real Element of REAL
less_dom ((M + f),B) is set
r /\ (less_dom ((M + f),B)) is Element of bool X
c7 is V7() V10( RAT ) V11(S) Function-like V32( RAT ,S) Element of bool [:RAT,S:]
rng c7 is Element of bool S
bool S is non empty set
union (rng c7) is set
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
F is V24() real ext-real rational set
c7 . F is set
R_EAL F is ext-real Element of ExtREAL
less_dom ((R_EAL M),(R_EAL F)) is Element of bool X
r /\ (less_dom ((R_EAL M),(R_EAL F))) is Element of bool X
B - F is V24() real ext-real Element of REAL
R_EAL (B - F) is ext-real Element of ExtREAL
less_dom ((R_EAL f),(R_EAL (B - F))) is Element of bool X
r /\ (less_dom ((R_EAL f),(R_EAL (B - F)))) is Element of bool X
(r /\ (less_dom ((R_EAL M),(R_EAL F)))) /\ (r /\ (less_dom ((R_EAL f),(R_EAL (B - F))))) is Element of bool X
(R_EAL M) + (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL B is ext-real Element of ExtREAL
less_dom (((R_EAL M) + (R_EAL f)),(R_EAL B)) is Element of bool X
r /\ (less_dom (((R_EAL M) + (R_EAL f)),(R_EAL B))) is Element of bool X
R_EAL (M + f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
[:RAT,S:] is non empty set
bool [:RAT,S:] is non empty set
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
B is V24() real ext-real Element of REAL
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
c7 is V7() V10( RAT ) V11(S) Function-like V32( RAT ,S) Element of bool [:RAT,S:]
F is V24() real ext-real rational set
c7 . F is set
R_EAL F is ext-real Element of ExtREAL
less_dom ((R_EAL M),(R_EAL F)) is Element of bool X
r /\ (less_dom ((R_EAL M),(R_EAL F))) is Element of bool X
B - F is V24() real ext-real Element of REAL
R_EAL (B - F) is ext-real Element of ExtREAL
less_dom ((R_EAL f),(R_EAL (B - F))) is Element of bool X
r /\ (less_dom ((R_EAL f),(R_EAL (B - F)))) is Element of bool X
(r /\ (less_dom ((R_EAL M),(R_EAL F)))) /\ (r /\ (less_dom ((R_EAL f),(R_EAL (B - F))))) is Element of bool X
less_dom (M,F) is set
r /\ (less_dom (M,F)) is Element of bool X
less_dom (f,(B - F)) is set
r /\ (less_dom (f,(B - F))) is Element of bool X
(r /\ (less_dom (M,F))) /\ (r /\ (less_dom (f,(B - F)))) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M + f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL M) + (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (M + f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL S) - (R_EAL M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
- M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- 1 is V24() real ext-real non positive rational set
(- 1) (#) M is V7() Function-like set
R_EAL (- M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL S) + (R_EAL (- M)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
S - M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- M is V7() Function-like V66() set
S + (- M) is V7() Function-like set
R_EAL (S - M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
S + (- M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL (S + (- M)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(- 1) (#) S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL ((- 1) (#) S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- 1 is V24() real ext-real non positive rational set
(- 1) (#) S is V7() Function-like set
R_EAL (- S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(- 1) (#) (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
M - f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- f is V7() Function-like V66() set
- 1 is V24() real ext-real non positive rational set
(- 1) (#) f is V7() Function-like set
M + (- f) is V7() Function-like set
r is Element of S
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
(- 1) (#) (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
- f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL (- f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL M is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL M) + (R_EAL (- f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (M - f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (max+ (R_EAL S)) is Element of bool X
bool X is non empty set
dom (R_EAL S) is Element of bool X
dom (max+ S) is Element of bool X
M is set
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
S . M is V24() real ext-real Element of REAL
max+ (S . M) is V24() real ext-real Element of REAL
max ((S . M),0) is V24() real ext-real set
(max+ S) . M is V24() real ext-real Element of REAL
dom (max- (R_EAL S)) is Element of bool X
dom (max- S) is Element of bool X
M is set
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
S . M is V24() real ext-real Element of REAL
R_EAL (S . M) is ext-real Element of ExtREAL
- (R_EAL (S . M)) is ext-real Element of ExtREAL
max ((- (R_EAL (S . M))),0.) is ext-real set
max- (S . M) is V24() real ext-real Element of REAL
- (S . M) is V24() real ext-real set
max ((- (S . M)),0) is V24() real ext-real set
(max- S) . M is V24() real ext-real Element of REAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is Element of X
(max+ S) . M is V24() real ext-real Element of REAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is Element of X
(max- S) . M is V24() real ext-real Element of REAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- 1 is V24() real ext-real non positive rational set
(- 1) (#) S is V7() Function-like set
max+ (- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
max+ (- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (- S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
max+ (R_EAL (- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max+ S) . M is V24() real ext-real Element of REAL
(max- S) . M is V24() real ext-real Element of REAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max- S) . M is V24() real ext-real Element of REAL
(max+ S) . M is V24() real ext-real Element of REAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max+ S) - (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- (max- S) is V7() Function-like V66() set
- 1 is V24() real ext-real non positive rational set
(- 1) (#) (max- S) is V7() Function-like set
(max+ S) + (- (max- S)) is V7() Function-like set
dom ((max+ S) - (max- S)) is Element of bool X
(max+ S) + (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((max+ S) + (max- S)) is Element of bool X
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) - (max- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((max+ (R_EAL S)) - (max- (R_EAL S))) is Element of bool X
R_EAL (max+ S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL (max+ S)) - (max- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((R_EAL (max+ S)) - (max- (R_EAL S))) is Element of bool X
R_EAL (max- S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL (max+ S)) - (R_EAL (max- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((R_EAL (max+ S)) - (R_EAL (max- S))) is Element of bool X
R_EAL ((max+ S) - (max- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL ((max+ S) - (max- S))) is Element of bool X
(max+ (R_EAL S)) + (max- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((max+ (R_EAL S)) + (max- (R_EAL S))) is Element of bool X
(R_EAL (max+ S)) + (max- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((R_EAL (max+ S)) + (max- (R_EAL S))) is Element of bool X
(R_EAL (max+ S)) + (R_EAL (max- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((R_EAL (max+ S)) + (R_EAL (max- S))) is Element of bool X
R_EAL ((max+ S) + (max- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL ((max+ S) + (max- S))) is Element of bool X
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max+ S) . M is V24() real ext-real Element of REAL
S . M is V24() real ext-real Element of REAL
(max- S) . M is V24() real ext-real Element of REAL
- (S . M) is V24() real ext-real Element of REAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
(R_EAL S) . M is ext-real Element of ExtREAL
- ((R_EAL S) . M) is ext-real Element of ExtREAL
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max+ S) . M is V24() real ext-real Element of REAL
S . M is V24() real ext-real Element of REAL
(max- S) . M is V24() real ext-real Element of REAL
R_EAL (S . M) is ext-real Element of ExtREAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max+ S) . M is V24() real ext-real Element of REAL
(max- S) . M is V24() real ext-real Element of REAL
S . M is V24() real ext-real Element of REAL
- (S . M) is V24() real ext-real Element of REAL
R_EAL 0 is ext-real Element of ExtREAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
(R_EAL S) . M is ext-real Element of ExtREAL
- ((R_EAL S) . M) is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max- S) . M is V24() real ext-real Element of REAL
S . M is V24() real ext-real Element of REAL
- (S . M) is V24() real ext-real Element of REAL
(max+ S) . M is V24() real ext-real Element of REAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
(R_EAL S) . M is ext-real Element of ExtREAL
- ((R_EAL S) . M) is ext-real Element of ExtREAL
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M is set
(max- S) . M is V24() real ext-real Element of REAL
(max+ S) . M is V24() real ext-real Element of REAL
S . M is V24() real ext-real Element of REAL
R_EAL 0 is ext-real Element of ExtREAL
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max- (R_EAL S)) . M is ext-real Element of ExtREAL
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) . M is ext-real Element of ExtREAL
(R_EAL S) . M is ext-real Element of ExtREAL
X is non empty set
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max+ S) - (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
- (max- S) is V7() Function-like V66() set
- 1 is V24() real ext-real non positive rational set
(- 1) (#) (max- S) is V7() Function-like set
(max+ S) + (- (max- S)) is V7() Function-like set
R_EAL S is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
max+ (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
max- (R_EAL S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(max+ (R_EAL S)) - (max- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (max+ S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL (max+ S)) - (max- (R_EAL S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (max- S) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL (max+ S)) - (R_EAL (max- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL ((max+ S) - (max- S)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
X is V24() real ext-real Element of REAL
|.X.| is V24() real ext-real Element of REAL
R_EAL X is ext-real Element of ExtREAL
|.(