:: MESFUNC6 semantic presentation

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
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= 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
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= 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
c₇ is Element of X
f . c₇ is ext-real Element of ExtREAL
- +infty is ext-real Element of ExtREAL
|.(f . c₇).| is ext-real Element of ExtREAL
c₇ is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng c₇ is Element of bool S
bool S is non empty set
union (rng c₇) is set
dom c₇ 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
c₇ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c₇ is set
c₇ + 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 / (c₇ + 1) is V24() real ext-real non negative rational Element of COMPLEX
B - (1 / (c₇ + 1)) is V24() real ext-real Element of REAL
R_EAL (B - (1 / (c₇ + 1))) is ext-real Element of ExtREAL
great_dom ((R_EAL r),(R_EAL (B - (1 / (c₇ + 1))))) is Element of bool X
S /\ (great_dom ((R_EAL r),(R_EAL (B - (1 / (c₇ + 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
c₇ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c₇ is set
c₇ + 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 / (c₇ + 1) is V24() real ext-real non negative rational Element of COMPLEX
B + (1 / (c₇ + 1)) is V24() real ext-real Element of REAL
R_EAL (B + (1 / (c₇ + 1))) is ext-real Element of ExtREAL
less_dom ((R_EAL r),(R_EAL (B + (1 / (c₇ + 1))))) is Element of bool X
S /\ (less_dom ((R_EAL r),(R_EAL (B + (1 / (c₇ + 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
c₇ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c₇ is set
c₇ + 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 / (c₇ + 1) is V24() real ext-real non negative rational Element of COMPLEX
B - (1 / (c₇ + 1)) is V24() real ext-real Element of REAL
R_EAL (B - (1 / (c₇ + 1))) is ext-real Element of ExtREAL
less_eq_dom ((R_EAL r),(R_EAL (B - (1 / (c₇ + 1))))) is Element of bool X
S /\ (less_eq_dom ((R_EAL r),(R_EAL (B - (1 / (c₇ + 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
c₇ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
f . c₇ is set
c₇ + 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 / (c₇ + 1) is V24() real ext-real non negative rational Element of COMPLEX
B + (1 / (c₇ + 1)) is V24() real ext-real Element of REAL
R_EAL (B + (1 / (c₇ + 1))) is ext-real Element of ExtREAL
great_eq_dom ((R_EAL r),(R_EAL (B + (1 / (c₇ + 1))))) is Element of bool X
S /\ (great_eq_dom ((R_EAL r),(R_EAL (B + (1 / (c₇ + 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
c₇ is V7() V10( RAT ) V11(S) Function-like V32( RAT ,S) Element of bool [:RAT,S:]
rng c₇ is Element of bool S
bool S is non empty set
union (rng c₇) 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
c₇ . 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:]
c₇ is V7() V10( RAT ) V11(S) Function-like V32( RAT ,S) Element of bool [:RAT,S:]
F is V24() real ext-real rational set
c₇ . 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
|.(R_EAL X).| is ext-real Element of ExtREAL
- (R_EAL X) is ext-real Element of ExtREAL
- X is V24() real ext-real Element of REAL
R_EAL (- X) 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:]
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:]
[: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:]
|.(R_EAL S).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL (abs S)) is Element of bool X
bool X is non empty set
dom S is Element of bool X
dom |.(R_EAL S).| is Element of bool X
M is set
(R_EAL (abs S)) . M is ext-real Element of ExtREAL
S . M is V24() real ext-real Element of REAL
|.(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
|.(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:]
abs 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:]
R_EAL (abs 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:]
|.(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) 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 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:]
max+ 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
max+ (R_EAL M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (max+ M) 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:]
dom M is Element of bool X
max- 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
max- (R_EAL M) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (max- M) 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:]
dom M is Element of bool X
abs 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_EAL M).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (abs M) 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
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:]
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
dom M is Element of bool X
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
dom (R_EAL M) is Element of bool X
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
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
X is set
[:X,REAL:] is 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:]
rng S is V59() V60() V61() Element of bool REAL
M is set
dom S is Element of bool X
bool X is non empty set
S . M is V24() real ext-real Element of REAL
M is ext-real Element of ExtREAL
rng S is V59() V60() V61() set
f is set
S . f is V24() real ext-real Element of REAL
X is set
[:X,REAL:] is 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 ext-real Element of ExtREAL
rng S is V59() V60() V61() set
rng S is V59() V60() V61() Element of bool REAL
f is set
S . f is V24() real ext-real Element of REAL
X is set
[:X,REAL:] is 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:]
rng S is V59() V60() V61() Element of bool REAL
M is set
dom S is Element of bool X
bool X is non empty set
S . M is V24() real ext-real Element of REAL
M is ext-real Element of ExtREAL
rng S is V59() V60() V61() set
f is set
S . f 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 ext-real Element of ExtREAL
rng S is V59() V60() V61() set
rng S is V59() V60() V61() Element of bool REAL
f is set
S . f 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 set
M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M | S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
rng M is V59() V60() V61() Element of bool REAL
f is ext-real Element of ExtREAL
rng (M | S) is V59() V60() V61() Element of bool REAL
dom (M | S) is Element of bool X
bool X is non empty set
r is set
(M | S) . r is V24() real ext-real Element of REAL
dom M is Element of bool X
(dom M) /\ S is Element of bool X
M . r 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:]
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:]
dom (S + M) is Element of bool X
bool X is non empty set
f is set
(S + M) . f is V24() real ext-real Element of REAL
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
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:]
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:]
f is set
dom (M (#) S) is Element of bool X
bool X is non empty set
S . f is V24() real ext-real Element of REAL
0 * M is V24() real ext-real Element of REAL
M * (S . f) is V24() real ext-real Element of REAL
(M (#) S) . f is V24() real ext-real Element of REAL
f is set
S . f is V24() real ext-real Element of REAL
M * (S . f) is V24() real ext-real Element of REAL
M * 0 is V24() real ext-real Element of REAL
(M (#) S) . f 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 V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
(dom S) /\ (dom M) is Element of bool X
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
f is set
dom (S - M) is Element of bool X
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
[: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:]
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:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(S + M) + f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,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:]
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:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(S + M) + f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((S + M) + f) is Element of bool X
bool X is non empty set
r is set
((S + M) + f) . r is V24() real ext-real Element of REAL
S . r is V24() real ext-real Element of REAL
M . r is V24() real ext-real Element of REAL
(S . r) + (M . r) is V24() real ext-real Element of REAL
f . r is V24() real ext-real Element of REAL
((S . r) + (M . r)) + (f . r) is V24() real ext-real Element of REAL
dom (S + M) is Element of bool X
dom f is Element of bool X
(dom (S + M)) /\ (dom f) is Element of bool X
(S + M) . r is V24() real ext-real Element of REAL
((S + M) . r) + (f . r) 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:]
max- S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (max+ S) is Element of bool X
bool X is non empty set
M is set
(max+ S) . M is V24() real ext-real Element of REAL
dom (max- S) is Element of bool X
M is 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:]
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:]
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:]
max+ (S + M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max+ (S + M)) + (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((max+ (S + M)) + (max- S)) is Element of bool X
dom M is Element of bool X
(dom S) /\ (dom M) is Element of bool X
max- (S + M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max- (S + M)) + (max+ S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((max- (S + M)) + (max+ S)) is Element of bool X
max- M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
((max+ (S + M)) + (max- S)) + (max- M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (((max+ (S + M)) + (max- S)) + (max- M)) is Element of bool X
max+ M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
((max- (S + M)) + (max+ S)) + (max+ M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (((max- (S + M)) + (max+ S)) + (max+ M)) is Element of bool X
dom (max- S) is Element of bool X
dom (max+ (S + M)) is Element of bool X
(dom (max+ (S + M))) /\ (dom (max- S)) is Element of bool X
dom (max+ S) is Element of bool X
dom (max- (S + M)) is Element of bool X
(dom (max- (S + M))) /\ (dom (max+ S)) is Element of bool X
dom (S + M) is Element of bool X
(dom S) /\ (dom S) is Element of bool X
(dom M) /\ ((dom S) /\ (dom S)) is Element of bool X
dom (max- M) is Element of bool X
((dom S) /\ (dom M)) /\ (dom M) is Element of bool X
(dom M) /\ (dom M) is Element of bool X
(dom S) /\ ((dom M) /\ (dom M)) is Element of bool X
dom (max+ M) is Element of bool X
f is set
(max+ (S + M)) . f is V24() real ext-real Element of REAL
(max- S) . f is V24() real ext-real Element of REAL
0 + 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
((max+ (S + M)) . f) + ((max- S) . f) is V24() real ext-real Element of REAL
((max+ (S + M)) + (max- S)) . f is V24() real ext-real Element of REAL
f is set
(max- (S + M)) . f is V24() real ext-real Element of REAL
(max+ S) . f is V24() real ext-real Element of REAL
((max- (S + M)) . f) + ((max+ S) . f) is V24() real ext-real Element of REAL
((max- (S + M)) + (max+ S)) . f 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:]
max+ S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
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:]
max+ (S + M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max+ (S + M)) + (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
((max+ (S + M)) + (max- S)) + (max- M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- (S + M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max- (S + M)) + (max+ S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
((max- (S + M)) + (max+ S)) + (max+ M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (max+ (S + M)) is Element of bool X
bool X is non empty set
dom (S + M) is Element of bool X
dom (max+ M) is Element of bool X
dom M is Element of bool X
dom (max+ S) is Element of bool X
dom S is Element of bool X
dom (max- S) is Element of bool X
dom (max- M) is Element of bool X
dom (((max+ (S + M)) + (max- S)) + (max- M)) is Element of bool X
dom ((max+ (S + M)) + (max- S)) is Element of bool X
(dom ((max+ (S + M)) + (max- S))) /\ (dom (max- M)) is Element of bool X
(dom (S + M)) /\ (dom S) is Element of bool X
((dom (S + M)) /\ (dom S)) /\ (dom M) is Element of bool X
(dom S) /\ (dom M) is Element of bool X
(dom (S + M)) /\ ((dom S) /\ (dom M)) is Element of bool X
dom (max- (S + M)) is Element of bool X
f is set
(((max+ (S + M)) + (max- S)) + (max- M)) . f is V24() real ext-real Element of REAL
(((max- (S + M)) + (max+ S)) + (max+ M)) . f is V24() real ext-real Element of REAL
(max+ M) . f is V24() real ext-real Element of REAL
M . f is V24() real ext-real Element of REAL
max+ (M . f) is V24() real ext-real Element of REAL
max ((M . f),0) is V24() real ext-real set
(max- M) . f is V24() real ext-real Element of REAL
max- (M . f) is V24() real ext-real Element of REAL
- (M . f) is V24() real ext-real set
max ((- (M . f)),0) is V24() real ext-real set
(max+ (S + M)) . f is V24() real ext-real Element of REAL
(S + M) . f is V24() real ext-real Element of REAL
max+ ((S + M) . f) is V24() real ext-real Element of REAL
max (((S + M) . f),0) is V24() real ext-real set
S . f is V24() real ext-real Element of REAL
(S . f) + (M . f) is V24() real ext-real Element of REAL
max (((S . f) + (M . f)),0) is V24() real ext-real set
(max+ S) . f is V24() real ext-real Element of REAL
max+ (S . f) is V24() real ext-real Element of REAL
max ((S . f),0) is V24() real ext-real set
(max- (S + M)) . f is V24() real ext-real Element of REAL
max- ((S + M) . f) is V24() real ext-real Element of REAL
- ((S + M) . f) is V24() real ext-real set
max ((- ((S + M) . f)),0) is V24() real ext-real set
- ((S . f) + (M . f)) is V24() real ext-real Element of REAL
max ((- ((S . f) + (M . f))),0) is V24() real ext-real set
(max- S) . f is V24() real ext-real Element of REAL
max- (S . f) is V24() real ext-real Element of REAL
- (S . f) is V24() real ext-real set
max ((- (S . f)),0) is V24() real ext-real set
- (M . f) is V24() real ext-real Element of REAL
((max- (S + M)) . f) + ((max+ S) . f) is V24() real ext-real Element of REAL
(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is V24() real ext-real Element of REAL
(- ((S . f) + (M . f))) + (S . f) is V24() real ext-real Element of REAL
((- ((S . f) + (M . f))) + (S . f)) + 0 is V24() real ext-real Element of REAL
((max+ (S + M)) . f) + ((max- S) . f) is V24() real ext-real Element of REAL
(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is V24() real ext-real Element of REAL
((S . f) + (M . f)) + 0 is V24() real ext-real Element of REAL
(((S . f) + (M . f)) + 0) + (- (M . f)) is V24() real ext-real Element of REAL
- (S . f) is V24() real ext-real Element of REAL
(- ((S . f) + (M . f))) + 0 is V24() real ext-real Element of REAL
((- ((S . f) + (M . f))) + 0) + (M . f) is V24() real ext-real Element of REAL
(- (M . f)) + (M . f) is V24() real ext-real Element of REAL
(- (S . f)) + ((- (M . f)) + (M . f)) is V24() real ext-real Element of REAL
((S . f) + (M . f)) + (- (S . f)) is V24() real ext-real Element of REAL
(((S . f) + (M . f)) + (- (S . f))) + 0 is V24() real ext-real Element of REAL
((- ((S . f) + (M . f))) + 0) + 0 is V24() real ext-real Element of REAL
0 + (- (S . f)) is V24() real ext-real Element of REAL
(0 + (- (S . f))) + (- (M . f)) is V24() real ext-real Element of REAL
dom (((max- (S + M)) + (max+ S)) + (max+ M)) is Element of bool X
dom (((max- (S + M)) + (max+ S)) + (max+ M)) 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:]
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 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:]
max+ (M (#) S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M (#) (max+ S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- (M (#) S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M (#) (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (max+ (M (#) S)) is Element of bool X
bool X is non empty set
dom (M (#) S) is Element of bool X
dom S is Element of bool X
dom (max+ S) is Element of bool X
dom (M (#) (max+ S)) is Element of bool X
f is Element of X
(max+ (M (#) S)) . f is V24() real ext-real Element of REAL
(M (#) (max+ S)) . f is V24() real ext-real Element of REAL
(M (#) S) . f is V24() real ext-real Element of REAL
max+ ((M (#) S) . f) is V24() real ext-real Element of REAL
max (((M (#) S) . f),0) is V24() real ext-real set
S . f is V24() real ext-real Element of REAL
M * (S . f) is V24() real ext-real Element of REAL
max ((M * (S . f)),0) is V24() real ext-real set
(max+ S) . f is V24() real ext-real Element of REAL
M * ((max+ S) . f) is V24() real ext-real Element of REAL
max+ (S . f) is V24() real ext-real Element of REAL
max ((S . f),0) is V24() real ext-real set
M * (max+ (S . f)) is V24() real ext-real Element of REAL
M * 0 is V24() real ext-real Element of REAL
max ((M * (S . f)),(M * 0)) is V24() real ext-real set
dom (max- (M (#) S)) is Element of bool X
dom (max- S) is Element of bool X
dom (M (#) (max- S)) is Element of bool X
f is Element of X
(max- (M (#) S)) . f is V24() real ext-real Element of REAL
(M (#) (max- S)) . f is V24() real ext-real Element of REAL
(M (#) S) . f is V24() real ext-real Element of REAL
max- ((M (#) S) . f) is V24() real ext-real Element of REAL
- ((M (#) S) . f) is V24() real ext-real set
max ((- ((M (#) S) . f)),0) is V24() real ext-real set
S . f is V24() real ext-real Element of REAL
M * (S . f) is V24() real ext-real Element of REAL
- (M * (S . f)) is V24() real ext-real Element of REAL
max ((- (M * (S . f))),0) is V24() real ext-real set
(max- S) . f is V24() real ext-real Element of REAL
M * ((max- S) . f) is V24() real ext-real Element of REAL
max- (S . f) is V24() real ext-real Element of REAL
- (S . f) is V24() real ext-real set
max ((- (S . f)),0) is V24() real ext-real set
M * (max- (S . f)) is V24() real ext-real Element of REAL
- (S . f) is V24() real ext-real Element of REAL
M * (- (S . f)) is V24() real ext-real Element of REAL
M * 0 is V24() real ext-real Element of REAL
max ((M * (- (S . f))),(M * 0)) is V24() real ext-real set
max ((- (M * (S . f))),(M * 0)) is V24() real ext-real 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:]
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 V24() real ext-real Element of REAL
- 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:]
max+ ((- M) (#) S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M (#) (max- S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- ((- M) (#) S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M (#) (max+ S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (max+ ((- M) (#) S)) is Element of bool X
bool X is non empty set
dom ((- M) (#) S) is Element of bool X
dom S is Element of bool X
dom (max- S) is Element of bool X
dom (M (#) (max- S)) is Element of bool X
f is Element of X
(max+ ((- M) (#) S)) . f is V24() real ext-real Element of REAL
(M (#) (max- S)) . f is V24() real ext-real Element of REAL
((- M) (#) S) . f is V24() real ext-real Element of REAL
max+ (((- M) (#) S) . f) is V24() real ext-real Element of REAL
max ((((- M) (#) S) . f),0) is V24() real ext-real set
S . f is V24() real ext-real Element of REAL
(- M) * (S . f) is V24() real ext-real Element of REAL
max (((- M) * (S . f)),0) is V24() real ext-real set
(max- S) . f is V24() real ext-real Element of REAL
M * ((max- S) . f) is V24() real ext-real Element of REAL
max- (S . f) is V24() real ext-real Element of REAL
- (S . f) is V24() real ext-real set
max ((- (S . f)),0) is V24() real ext-real set
M * (max- (S . f)) is V24() real ext-real Element of REAL
- (S . f) is V24() real ext-real Element of REAL
M * (- (S . f)) is V24() real ext-real Element of REAL
M * 0 is V24() real ext-real Element of REAL
max ((M * (- (S . f))),(M * 0)) is V24() real ext-real set
dom (max- ((- M) (#) S)) is Element of bool X
dom (max+ S) is Element of bool X
dom (M (#) (max+ S)) is Element of bool X
f is Element of X
(max- ((- M) (#) S)) . f is V24() real ext-real Element of REAL
(M (#) (max+ S)) . f is V24() real ext-real Element of REAL
((- M) (#) S) . f is V24() real ext-real Element of REAL
max- (((- M) (#) S) . f) is V24() real ext-real Element of REAL
- (((- M) (#) S) . f) is V24() real ext-real set
max ((- (((- M) (#) S) . f)),0) is V24() real ext-real set
S . f is V24() real ext-real Element of REAL
(- M) * (S . f) is V24() real ext-real Element of REAL
- ((- M) * (S . f)) is V24() real ext-real Element of REAL
max ((- ((- M) * (S . f))),0) is V24() real ext-real set
(max+ S) . f is V24() real ext-real Element of REAL
M * ((max+ S) . f) is V24() real ext-real Element of REAL
max+ (S . f) is V24() real ext-real Element of REAL
max ((S . f),0) is V24() real ext-real set
M * (max+ (S . f)) is V24() real ext-real Element of REAL
M * (S . f) is V24() real ext-real Element of REAL
M * 0 is V24() real ext-real Element of REAL
max ((M * (S . f)),(M * 0)) is V24() real ext-real set
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 V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M | S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ (M | S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max+ M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max+ M) | S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- (M | S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
max- M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max- M) | S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (max+ (M | S)) is Element of bool X
bool X is non empty set
dom (M | S) is Element of bool X
dom M is Element of bool X
(dom M) /\ S is Element of bool X
dom (max+ M) is Element of bool X
(dom (max+ M)) /\ S is Element of bool X
dom ((max+ M) | S) is Element of bool X
f is Element of X
(max+ (M | S)) . f is V24() real ext-real Element of REAL
((max+ M) | S) . f is V24() real ext-real Element of REAL
(M | S) . f is V24() real ext-real Element of REAL
max+ ((M | S) . f) is V24() real ext-real Element of REAL
max (((M | S) . f),0) is V24() real ext-real set
M . f is V24() real ext-real Element of REAL
max ((M . f),0) is V24() real ext-real set
(max+ M) . f is V24() real ext-real Element of REAL
max+ (M . f) is V24() real ext-real Element of REAL
dom (max- (M | S)) is Element of bool X
dom (max- M) is Element of bool X
(dom (max- M)) /\ S is Element of bool X
dom ((max- M) | S) is Element of bool X
f is Element of X
(max- (M | S)) . f is V24() real ext-real Element of REAL
((max- M) | S) . f is V24() real ext-real Element of REAL
(M | S) . f is V24() real ext-real Element of REAL
max- ((M | S) . f) is V24() real ext-real Element of REAL
- ((M | S) . f) is V24() real ext-real set
max ((- ((M | S) . f)),0) is V24() real ext-real set
M . f is V24() real ext-real Element of REAL
- (M . f) is V24() real ext-real Element of REAL
max ((- (M . f)),0) is V24() real ext-real set
(max- M) . f is V24() real ext-real Element of REAL
max- (M . f) is V24() real ext-real Element of REAL
- (M . f) is V24() real ext-real set
max ((- (M . f)),0) is V24() real ext-real set
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 V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
M | S 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:]
dom (M + f) is Element of bool X
bool X is non empty set
(M + f) | S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((M + f) | S) is Element of bool X
f | S is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(M | S) + (f | S) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((M | S) + (f | S)) is Element of bool X
dom (M | S) is Element of bool X
dom (f | S) is Element of bool X
(dom (M | S)) /\ (dom (f | S)) is Element of bool X
dom M is Element of bool X
(dom M) /\ S is Element of bool X
((dom M) /\ S) /\ (dom (f | S)) is Element of bool X
dom f is Element of bool X
(dom f) /\ S is Element of bool X
((dom M) /\ S) /\ ((dom f) /\ S) is Element of bool X
((dom M) /\ S) /\ (dom f) is Element of bool X
(((dom M) /\ S) /\ (dom f)) /\ S is Element of bool X
(dom M) /\ (dom f) is Element of bool X
((dom M) /\ (dom f)) /\ S is Element of bool X
(((dom M) /\ (dom f)) /\ S) /\ S is Element of bool X
S /\ S is set
((dom M) /\ (dom f)) /\ (S /\ S) is Element of bool X
(dom (M + f)) /\ S is Element of bool X
r is set
((M + f) | S) . r is V24() real ext-real Element of REAL
(M + f) . r is V24() real ext-real Element of REAL
M . r is V24() real ext-real Element of REAL
f . r is V24() real ext-real Element of REAL
(M . r) + (f . r) is V24() real ext-real Element of REAL
(M | S) . r is V24() real ext-real Element of REAL
((M | S) . r) + (f . r) is V24() real ext-real Element of REAL
(f | S) . r is V24() real ext-real Element of REAL
((M | S) . r) + ((f | S) . r) is V24() real ext-real Element of REAL
((M | S) + (f | S)) . r 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:]
M is V24() real ext-real Element of REAL
eq_dom (S,M) is set
{M} is non empty V59() V60() V61() Element of bool REAL
S " {M} is Element of bool X
bool X is non empty set
f is set
S . f 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) . f is ext-real Element of ExtREAL
R_EAL M is ext-real Element of ExtREAL
dom S is Element of bool X
f is set
S . 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)
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_eq_dom (M,r) is set
f /\ (great_eq_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_eq_dom (M,r))) /\ (less_dom (M,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 B is ext-real Element of ExtREAL
less_dom ((R_EAL M),(R_EAL B)) is Element of bool X
f /\ (less_dom ((R_EAL M),(R_EAL B))) is Element of bool X
f /\ (less_dom (M,B)) is Element of bool X
(f /\ (great_eq_dom (M,r))) /\ (f /\ (less_dom (M,B))) is Element of bool X
(f /\ (great_eq_dom (M,r))) /\ f is Element of bool X
((f /\ (great_eq_dom (M,r))) /\ f) /\ (less_dom (M,B)) is Element of bool X
f /\ f is M7(X,S)
(great_eq_dom (M,r)) /\ (f /\ f) is Element of bool X
((great_eq_dom (M,r)) /\ (f /\ f)) /\ (less_dom (M,B)) 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
M | f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
r is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng r is Element of bool S
bool S is non empty set
union (rng r) is set
dom r is V59() V60() V61() V62() V63() V64() Element of bool NAT
len r is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
B is V7() Function-like FinSequence-like set
len B is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
dom B is V59() V60() V61() V62() V63() V64() Element of bool NAT
rng B is set
c₇ is set
F is set
B . F is set
n is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
Seg (len r) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
r . n is set
B . n is set
(r . n) /\ f is Element of bool X
Seg (len r) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len r ) } is set
c₇ is V7() V10( NAT ) V11(S) Function-like FinSequence-like FinSequence of S
dom c₇ 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
c₇ . F is set
c₇ . n is set
r . F is set
r . n is set
(r . F) /\ f is Element of bool X
(r . n) /\ f is Element of bool X
(c₇ . F) /\ (c₇ . n) is set
((r . F) /\ f) /\ (r . n) is Element of bool X
(((r . F) /\ f) /\ (r . n)) /\ f is Element of bool X
(r . F) /\ (r . n) is set
((r . F) /\ (r . n)) /\ f is Element of bool X
(((r . F) /\ (r . n)) /\ f) /\ f is Element of bool X
{} /\ f is V59() V60() V61() V62() V63() V64() Element of bool X
({} /\ f) /\ f is V59() V60() V61() V62() V63() V64() Element of bool X
F is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng F is Element of bool S
union (rng F) is set
dom (M | f) is Element of bool X
n is set
x is set
dom F is V59() V60() V61() V62() V63() V64() Element of bool NAT
y is set
F . y is set
FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
r . FG is set
F . FG is set
(r . FG) /\ f is Element of bool X
(dom M) /\ f is Element of bool X
n is set
(dom M) /\ f is Element of bool X
x is set
y is set
r . y is set
FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
dom F is V59() V60() V61() V62() V63() V64() Element of bool NAT
F . FG is set
r . FG is set
(r . FG) /\ f is Element of bool X
dom F is V59() V60() V61() V62() V63() V64() Element of bool NAT
n is ordinal natural V24() real ext-real non negative set
F . n is set
x is Element of X
y is Element of X
(M | f) . x is V24() real ext-real Element of REAL
(M | f) . y is V24() real ext-real Element of REAL
r . n is set
(r . n) /\ f is Element of bool X
M . x is V24() real ext-real Element of REAL
M . y 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)
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 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
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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
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 V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom r is Element of bool X
f + r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (f + r) is Element of bool X
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
B is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
c₇ is V7() V10( NAT ) V11( ExtREAL ) Function-like V67() FinSequence-like FinSequence of ExtREAL
len B is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
rng B is Element of bool S
bool S is non empty set
union (rng B) is set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
n is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
x is V7() V10( NAT ) V11( ExtREAL ) Function-like V67() FinSequence-like FinSequence of ExtREAL
len n is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(dom f) /\ (dom r) is Element of bool X
(len B) * (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
FG is V7() Function-like FinSequence-like set
len FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
dom FG is V59() V60() V61() V62() V63() V64() Element of bool NAT
Seg ((len B) * (len n)) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= (len B) * (len n) ) } is set
la9 is ordinal natural V24() real ext-real non negative set
la9 -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(la9 -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((la9 -' 1) div (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(la9 -' 1) mod (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((la9 -' 1) mod (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((len B) * (len n)) -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(((len B) * (len n)) -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
FG is ordinal natural V24() real ext-real non negative set
FG is ordinal natural V24() real ext-real non negative set
FG * FG is ordinal natural V24() real ext-real non negative set
0 + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(FG * FG) -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((FG * FG) -' 1) div FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(FG * FG) div FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((FG * FG) div FG) - 1 is V24() real ext-real rational Element of REAL
((len B) * (len n)) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
Seg (len B) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len B ) } is set
dom B is V59() V60() V61() V62() V63() V64() Element of bool NAT
B . (((la9 -' 1) div (len n)) + 1) is set
dom n is V59() V60() V61() V62() V63() V64() Element of bool NAT
n . (((la9 -' 1) mod (len n)) + 1) is set
rng n is Element of bool S
(B . (((la9 -' 1) div (len n)) + 1)) /\ (n . (((la9 -' 1) mod (len n)) + 1)) is set
FG . la9 is set
FG is V7() V10( NAT ) V11(S) Function-like FinSequence-like FinSequence of S
dom FG is V59() V60() V61() V62() V63() V64() Element of bool NAT
lb9 is ordinal natural V24() real ext-real non negative set
k is ordinal natural V24() real ext-real non negative set
FG . lb9 is set
FG . k is set
lb9 -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(lb9 -' 1) mod (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((lb9 -' 1) mod (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(lb9 -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((lb9 -' 1) div (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
B . (((lb9 -' 1) div (len n)) + 1) is set
n . (((lb9 -' 1) mod (len n)) + 1) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ (n . (((lb9 -' 1) mod (len n)) + 1)) is set
k -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(k -' 1) mod (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((k -' 1) mod (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(k -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((k -' 1) div (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
la9 is ordinal natural V24() real ext-real non negative set
FG is ordinal natural V24() real ext-real non negative set
FG * la9 is ordinal natural V24() real ext-real non negative set
(FG * la9) -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((FG * la9) -' 1) div la9 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(FG * la9) div la9 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((FG * la9) div la9) - 1 is V24() real ext-real rational Element of REAL
(k -' 1) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(((k -' 1) div (len n)) + 1) - 1 is V24() real ext-real rational Element of REAL
((((k -' 1) div (len n)) + 1) - 1) * (len n) is V24() real ext-real rational Element of REAL
(((k -' 1) mod (len n)) + 1) - 1 is V24() real ext-real rational Element of REAL
(((((k -' 1) div (len n)) + 1) - 1) * (len n)) + ((((k -' 1) mod (len n)) + 1) - 1) is V24() real ext-real rational Element of REAL
((((((k -' 1) div (len n)) + 1) - 1) * (len n)) + ((((k -' 1) mod (len n)) + 1) - 1)) + 1 is V24() real ext-real rational Element of REAL
k - 1 is V24() real ext-real Element of REAL
(k - 1) + 1 is V24() real ext-real Element of REAL
(((((k -' 1) div (len n)) + 1) - 1) * (len n)) + (((k -' 1) mod (len n)) + 1) is V24() real ext-real rational Element of REAL
(lb9 -' 1) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(((lb9 -' 1) div (len n)) + 1) - 1 is V24() real ext-real rational Element of REAL
((((lb9 -' 1) div (len n)) + 1) - 1) * (len n) is V24() real ext-real rational Element of REAL
(((lb9 -' 1) mod (len n)) + 1) - 1 is V24() real ext-real rational Element of REAL
(((((lb9 -' 1) div (len n)) + 1) - 1) * (len n)) + ((((lb9 -' 1) mod (len n)) + 1) - 1) is V24() real ext-real rational Element of REAL
((((((lb9 -' 1) div (len n)) + 1) - 1) * (len n)) + ((((lb9 -' 1) mod (len n)) + 1) - 1)) + 1 is V24() real ext-real rational Element of REAL
lb9 - 1 is V24() real ext-real Element of REAL
(lb9 - 1) + 1 is V24() real ext-real Element of REAL
(((((lb9 -' 1) div (len n)) + 1) - 1) * (len n)) + (((lb9 -' 1) mod (len n)) + 1) is V24() real ext-real rational Element of REAL
(((len B) * (len n)) div (len n)) - 1 is V24() real ext-real rational Element of REAL
(FG . lb9) /\ (FG . k) is set
B . (((k -' 1) div (len n)) + 1) is set
n . (((k -' 1) mod (len n)) + 1) is set
(B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
((B . (((lb9 -' 1) div (len n)) + 1)) /\ (n . (((lb9 -' 1) mod (len n)) + 1))) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(n . (((lb9 -' 1) mod (len n)) + 1)) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)))) is set
(n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
(B . (((k -' 1) div (len n)) + 1)) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)))) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ (B . (((k -' 1) div (len n)) + 1)) is set
((B . (((lb9 -' 1) div (len n)) + 1)) /\ (B . (((k -' 1) div (len n)) + 1))) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
{} /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is V59() V60() V61() V62() V63() V64() set
(FG . lb9) /\ (FG . k) is set
B . (((k -' 1) div (len n)) + 1) is set
n . (((k -' 1) mod (len n)) + 1) is set
(B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
((B . (((lb9 -' 1) div (len n)) + 1)) /\ (n . (((lb9 -' 1) mod (len n)) + 1))) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(n . (((lb9 -' 1) mod (len n)) + 1)) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)))) is set
(n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
(B . (((k -' 1) div (len n)) + 1)) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ ((B . (((k -' 1) div (len n)) + 1)) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)))) is set
(B . (((lb9 -' 1) div (len n)) + 1)) /\ (B . (((k -' 1) div (len n)) + 1)) is set
((B . (((lb9 -' 1) div (len n)) + 1)) /\ (B . (((k -' 1) div (len n)) + 1))) /\ ((n . (((lb9 -' 1) mod (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1))) is set
((B . (((lb9 -' 1) div (len n)) + 1)) /\ (B . (((k -' 1) div (len n)) + 1))) /\ {} is V59() V60() V61() V62() V63() V64() set
union (rng n) is set
FG is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng FG is Element of bool S
union (rng FG) is set
la9 is set
lb9 is set
k is ordinal natural V24() real ext-real non negative set
B . k is set
x is ordinal natural V24() real ext-real non negative set
1 + x is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
y is set
i is ordinal natural V24() real ext-real non negative set
n . i is set
Seg (len n) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
j is ordinal natural V24() real ext-real non negative set
1 + j is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
k - 1 is V24() real ext-real Element of REAL
(k - 1) * (len n) is V24() real ext-real Element of REAL
((k - 1) * (len n)) + i is V24() real ext-real Element of REAL
0 + i is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
k is ordinal natural V24() real ext-real non negative set
k -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
k - 1 is V24() real ext-real Element of REAL
x * (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(x * (len n)) + j is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(k -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((k -' 1) div (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(len B) - 1 is V24() real ext-real rational Element of REAL
((len B) - 1) * (len n) is V24() real ext-real rational Element of REAL
(((len B) - 1) * (len n)) + i is V24() real ext-real Element of REAL
(((len B) - 1) * (len n)) + (len n) is V24() real ext-real rational Element of REAL
dom FG is V59() V60() V61() V62() V63() V64() Element of bool NAT
FG . k is set
(k -' 1) mod (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((k -' 1) mod (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(B . k) /\ (n . i) is set
k is set
x is set
y is ordinal natural V24() real ext-real non negative set
FG . y is set
y -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(y -' 1) mod (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((y -' 1) mod (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(y -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((y -' 1) div (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
len FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
Seg (len FG) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len FG ) } is set
lb9 is ordinal natural V24() real ext-real non negative set
la9 is ordinal natural V24() real ext-real non negative set
la9 * lb9 is ordinal natural V24() real ext-real non negative set
(la9 * lb9) -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((la9 * lb9) -' 1) div lb9 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(la9 * lb9) div lb9 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((la9 * lb9) div lb9) - 1 is V24() real ext-real rational Element of REAL
(((len B) * (len n)) div (len n)) - 1 is V24() real ext-real rational Element of REAL
B . (((y -' 1) div (len n)) + 1) is set
n . (((y -' 1) mod (len n)) + 1) is set
(B . (((y -' 1) div (len n)) + 1)) /\ (n . (((y -' 1) mod (len n)) + 1)) is set
dom FG is V59() V60() V61() V62() V63() V64() Element of bool NAT
k is ordinal natural V24() real ext-real non negative set
FG . k is set
x is Element of X
y is Element of X
(f + r) . x is V24() real ext-real Element of REAL
(f + r) . y is V24() real ext-real Element of REAL
k -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(k -' 1) div (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((k -' 1) div (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(k -' 1) mod (len n) is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((k -' 1) mod (len n)) + 1 is non empty ordinal natural V24() real ext-real positive non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
len FG is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
Seg (len FG) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len FG ) } is set
Seg (len n) is V59() V60() V61() V62() V63() V64() Element of bool NAT
{ b₁ where b₁ is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT : ( 1 <= b₁ & b₁ <= len n ) } is set
lb9 is ordinal natural V24() real ext-real non negative set
la9 is ordinal natural V24() real ext-real non negative set
la9 * lb9 is ordinal natural V24() real ext-real non negative set
(la9 * lb9) -' 1 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((la9 * lb9) -' 1) div lb9 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
(la9 * lb9) div lb9 is ordinal natural V24() real ext-real non negative V29() V59() V60() V61() V62() V63() V64() rational Element of NAT
((la9 * lb9) div lb9) - 1 is V24() real ext-real rational Element of REAL
(((len B) * (len n)) div (len n)) - 1 is V24() real ext-real rational Element of REAL
B . (((k -' 1) div (len n)) + 1) is set
n . (((k -' 1) mod (len n)) + 1) is set
(B . (((k -' 1) div (len n)) + 1)) /\ (n . (((k -' 1) mod (len n)) + 1)) is set
r . x is V24() real ext-real Element of REAL
x . (((k -' 1) mod (len n)) + 1) is ext-real Element of ExtREAL
r . y is V24() real ext-real Element of REAL
f . x is V24() real ext-real Element of REAL
c₇ . (((k -' 1) div (len n)) + 1) is ext-real Element of ExtREAL
(f . x) + (r . x) is V24() real ext-real Element of REAL
(c₇ . (((k -' 1) div (len n)) + 1)) + (x . (((k -' 1) mod (len n)) + 1)) is ext-real Element of ExtREAL
f . y is V24() real ext-real Element of REAL
(f . y) + (r . y) 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)
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:]
dom (M + f) is Element of bool X
r is Element of S
<*r*> is V7() V10( NAT ) V11(S) Function-like FinSequence-like FinSequence of S
[1,r] is set
{1,r} is non empty set
{{1,r},{1}} is non empty set
{[1,r]} is non empty set
dom <*r*> is V59() V60() V61() V62() V63() V64() Element of bool NAT
c₇ is ordinal natural V24() real ext-real non negative set
F is ordinal natural V24() real ext-real non negative set
<*r*> . c₇ is set
<*r*> . F is set
c₇ is ordinal natural V24() real ext-real non negative set
<*r*> . c₇ is set
c₇ is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng c₇ is Element of bool S
bool S is non empty set
union (rng c₇) is set
dom c₇ is V59() V60() V61() V62() V63() V64() Element of bool NAT
bool {} is non empty Element of bool (bool {})
bool (bool {}) is non empty set
union (bool {}) is empty non proper V59() V60() V61() V62() V63() V64() V65() Element of bool {}
F is ordinal natural V24() real ext-real non negative set
n is Element of X
c₇ . F is set
x is Element of X
(M + f) . n is V24() real ext-real Element of REAL
(M + f) . x is V24() real ext-real Element of REAL
r is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng r is Element of bool S
bool S is non empty set
union (rng r) is set
dom r is V59() V60() V61() V62() V63() V64() Element of bool NAT
dom (M + f) is Element of bool X
dom M is Element of bool X
dom f is Element of bool X
(dom M) /\ (dom f) is Element of bool X
M | (dom (M + f)) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f | (dom (M + f)) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (M | (dom (M + f))) is Element of bool X
(dom M) /\ (dom (M + f)) is Element of bool X
(dom M) /\ (dom M) is Element of bool X
((dom M) /\ (dom M)) /\ (dom f) is Element of bool X
dom (f | (dom (M + f))) is Element of bool X
(dom f) /\ (dom (M + f)) is Element of bool X
(dom f) /\ (dom f) is Element of bool X
((dom f) /\ (dom f)) /\ (dom M) is Element of bool X
(M | (dom (M + f))) + (f | (dom (M + f))) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom ((M | (dom (M + f))) + (f | (dom (M + f)))) is Element of bool X
(dom (M | (dom (M + f)))) /\ (dom (f | (dom (M + f)))) is Element of bool X
r is Element of X
((M | (dom (M + f))) + (f | (dom (M + f)))) . r is V24() real ext-real Element of REAL
(M + f) . r is V24() real ext-real Element of REAL
(M | (dom (M + f))) . r is V24() real ext-real Element of REAL
(f | (dom (M + f))) . r is V24() real ext-real Element of REAL
((M | (dom (M + f))) . r) + ((f | (dom (M + f))) . r) is V24() real ext-real Element of REAL
M . r is V24() real ext-real Element of REAL
(M . r) + ((f | (dom (M + f))) . r) is V24() real ext-real Element of REAL
f . r is V24() real ext-real Element of REAL
(M . r) + (f . r) is V24() real ext-real Element of REAL
dom (M + 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 V24() real ext-real Element of REAL
f (#) M is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom M is Element of bool X
B is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng B is Element of bool S
bool S is non empty set
union (rng B) is set
dom B is V59() V60() V61() V62() V63() V64() Element of bool NAT
dom (f (#) M) is Element of bool X
c₇ is ordinal natural V24() real ext-real non negative set
F is Element of X
B . c₇ is set
n is Element of X
(f (#) M) . n is V24() real ext-real Element of REAL
M . n is V24() real ext-real Element of REAL
f * (M . n) is V24() real ext-real Element of REAL
(f (#) M) . F is V24() real ext-real Element of REAL
M . F is V24() real ext-real Element of REAL
f * (M . F) 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:]
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:]
- 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
dom (S - M) is Element of bool X
bool X is non empty set
dom S is Element of bool X
dom M is Element of bool X
(dom S) /\ (dom M) 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 Element of S
f is V24() real ext-real Element of REAL
r is set
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom r is Element of bool X
B is set
B is set
<*(dom r)*> is V7() V10( NAT ) V11( bool X) Function-like FinSequence-like FinSequence of bool X
[1,(dom r)] is set
{1,(dom r)} is non empty set
{{1,(dom r)},{1}} is non empty set
{[1,(dom r)]} is non empty set
rng <*(dom r)*> is Element of bool (bool X)
{(dom r)} is non empty Element of bool (bool X)
{M} is non empty Element of bool S
bool S is non empty set
F is ordinal natural V24() real ext-real non negative set
c₇ is V7() V10( NAT ) V11(S) Function-like FinSequence-like FinSequence of S
dom c₇ is V59() V60() V61() V62() V63() V64() Element of bool NAT
n is ordinal natural V24() real ext-real non negative set
c₇ . F is set
c₇ . n is set
F is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng F is Element of bool S
union (rng F) is set
dom F is V59() V60() V61() V62() V63() V64() Element of bool NAT
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
r . x is V24() real ext-real Element of REAL
r . y is V24() real ext-real Element of REAL
B is V7() V10( NAT ) V11(S) Function-like FinSequence-like V120() FinSequence of S
rng B is Element of bool S
bool S is non empty set
union (rng B) is set
dom B is V59() V60() V61() V62() V63() V64() Element of bool NAT
B is set
r . 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 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
(dom M) /\ f is Element of bool X
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
c₇ is set
dom (M | f) is Element of bool X
B is V24() real ext-real set
R_EAL B is ext-real Element of ExtREAL
(M | f) . c₇ is V24() real ext-real Element of REAL
less_dom ((M | f),B) is set
M . c₇ is V24() real ext-real Element of REAL
r /\ (less_dom ((M | f),B)) is Element of bool X
less_dom (M,B) is set
f /\ (less_dom (M,B)) is Element of bool X
less_dom ((M | f),(R_EAL B)) is set
r /\ (less_dom ((M | f),(R_EAL B))) 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
max- 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:]
max+ (M + f) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max+ (M + f)) + (max- M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
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
max+ 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
(dom M) /\ (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:]
max- (M + f) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(max- (M + f)) + (max+ M) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
dom (M + 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:]
dom M is Element of bool X
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:]
dom (M + f) is Element of bool X
r is Element of S
B is Element of S
r /\ B is M7(X,S)
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 Element of S
f /\ r is M7(X,S)
c₇ is set
B is V24() real ext-real set
less_dom (M,B) is set
f /\ (less_dom (M,B)) is Element of bool X
B is V24() real ext-real set
less_dom (M,B) is set
(f /\ r) /\ (less_dom (M,B)) is Element of bool X
f /\ (less_dom (M,B)) is Element of bool X
r /\ (f /\ (less_dom (M,B))) is Element of bool X
r /\ (less_dom (M,B)) is Element of bool X
B is V24() real ext-real set
less_dom (M,B) is set
(f /\ r) /\ (less_dom (M,B)) is Element of bool X
f /\ (less_dom (M,B)) is Element of bool X
r /\ (f /\ (less_dom (M,B))) is Element of bool X
r /\ (less_dom (M,B)) 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
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:]
B is Element of S
f /\ B is M7(X,S)
dom (r (#) M) is Element of bool X
X is non empty set
bool X is non empty set
bool (bool X) 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
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,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:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
integral+ (M,(R_EAL f)) is ext-real Element of ExtREAL
r is Element of S
r is Element of S
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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
integral+ (M,(R_EAL f)) is ext-real Element of ExtREAL
integral' (M,(R_EAL f)) is ext-real Element of ExtREAL
dom (R_EAL f) is Element of bool X
r is Element of S
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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
r is Element of S
r is Element of S
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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
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
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | 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
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) is ext-real Element of ExtREAL
B is Element of S
r \/ B is M7(X,S)
f | (r \/ B) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | (r \/ B))) is ext-real Element of ExtREAL
R_EAL (f | (r \/ B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | (r \/ B)))) is ext-real Element of ExtREAL
max+ (R_EAL (f | (r \/ B))) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | (r \/ B))))) is ext-real Element of ExtREAL
max- (R_EAL (f | (r \/ B))) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | (r \/ B))))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | (r \/ B)))))) - (integral+ (M,(max- (R_EAL (f | (r \/ B)))))) is ext-real Element of ExtREAL
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
(X,S,M,(f | r)) + (X,S,M,(f | B)) is ext-real Element of ExtREAL
c₇ is Element of S
c₇ is Element of S
R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
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
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | 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
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) is ext-real Element of ExtREAL
B is Element of S
B is Element of S
R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
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
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | 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
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) is ext-real Element of ExtREAL
B is Element of S
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
c₇ is Element of S
c₇ is Element of S
R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
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
M . r is ext-real Element of ExtREAL
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | 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
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) is ext-real Element of ExtREAL
B is Element of S
B is Element of S
R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
r is Element of S
B is Element of S
M . B is ext-real Element of ExtREAL
r \ B is M7(X,S)
f | (r \ B) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | (r \ B))) is ext-real Element of ExtREAL
R_EAL (f | (r \ B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | (r \ B)))) is ext-real Element of ExtREAL
max+ (R_EAL (f | (r \ B))) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | (r \ B))))) is ext-real Element of ExtREAL
max- (R_EAL (f | (r \ B))) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | (r \ B))))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | (r \ B)))))) - (integral+ (M,(max- (R_EAL (f | (r \ B)))))) is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool X) 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
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
f | r 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:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL (f | r) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | 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
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) is ext-real Element of ExtREAL
B is Element of S
r \/ B is M7(X,S)
f | (r \/ B) is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | (r \/ B))) is ext-real Element of ExtREAL
R_EAL (f | (r \/ B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | (r \/ B)))) is ext-real Element of ExtREAL
max+ (R_EAL (f | (r \/ B))) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | (r \/ B))))) is ext-real Element of ExtREAL
max- (R_EAL (f | (r \/ B))) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | (r \/ B))))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | (r \/ B)))))) - (integral+ (M,(max- (R_EAL (f | (r \/ B)))))) is ext-real Element of ExtREAL
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
(X,S,M,(f | r)) + (X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
r is Element of S
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) is ext-real Element of ExtREAL
B is Element of S
(dom f) \ B is Element of bool X
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
(X,S,M,(f | B)) + (X,S,M,(f | r)) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
abs f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
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
|.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (abs 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
|.(X,S,M,f).| is ext-real Element of ExtREAL
abs f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(abs f)) is ext-real Element of ExtREAL
R_EAL (abs f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (abs f))) is ext-real Element of ExtREAL
max+ (R_EAL (abs f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (abs f)))) is ext-real Element of ExtREAL
max- (R_EAL (abs f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (abs f)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (abs f))))) - (integral+ (M,(max- (R_EAL (abs f))))) is ext-real Element of ExtREAL
|.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,|.(R_EAL f).|) is ext-real Element of ExtREAL
max+ |.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ |.(R_EAL f).|)) is ext-real Element of ExtREAL
max- |.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- |.(R_EAL f).|)) is ext-real Element of ExtREAL
(integral+ (M,(max+ |.(R_EAL f).|))) - (integral+ (M,(max- |.(R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
abs f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(abs f)) is ext-real Element of ExtREAL
R_EAL (abs 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
Integral (M,(R_EAL (abs f))) is ext-real Element of ExtREAL
max+ (R_EAL (abs f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (abs f)))) is ext-real Element of ExtREAL
max- (R_EAL (abs f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (abs f)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (abs f))))) - (integral+ (M,(max- (R_EAL (abs f))))) is ext-real Element of ExtREAL
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom r is Element of bool X
(X,S,M,r) is ext-real Element of ExtREAL
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL r)) is ext-real Element of ExtREAL
max+ (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL r))) is ext-real Element of ExtREAL
max- (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL r))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL r)))) - (integral+ (M,(max- (R_EAL r)))) is ext-real Element of ExtREAL
B is Element of X
f . B is V24() real ext-real Element of REAL
abs (f . B) is V24() real ext-real Element of REAL
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL f) . B is ext-real Element of ExtREAL
|.((R_EAL f) . B).| is ext-real Element of ExtREAL
dom (R_EAL f) is Element of bool X
(R_EAL r) . B is ext-real Element of ExtREAL
B is Element of S
B is Element of S
|.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,|.(R_EAL f).|) is ext-real Element of ExtREAL
max+ |.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ |.(R_EAL f).|)) is ext-real Element of ExtREAL
max- |.(R_EAL f).| is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- |.(R_EAL f).|)) is ext-real Element of ExtREAL
(integral+ (M,(max+ |.(R_EAL f).|))) - (integral+ (M,(max- |.(R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom f is Element of bool X
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
M . (dom f) is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r) * (M . (dom f)) is ext-real Element of ExtREAL
dom (R_EAL f) is Element of bool X
B is set
(R_EAL f) . B is ext-real Element of ExtREAL
B is Element of S
M . (dom (R_EAL f)) is ext-real Element of ExtREAL
(R_EAL r) * (M . (dom (R_EAL f))) is ext-real Element of ExtREAL
integral' (M,(R_EAL f)) is ext-real Element of ExtREAL
integral+ (M,(R_EAL 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f + r 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:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL f) + (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (f + r) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f + r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (f + r) is Element of bool X
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
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL f) + (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((R_EAL f) + (R_EAL r)) is Element of bool X
R_EAL (f + r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL (f + 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f + r 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:]
[:X,ExtREAL:] is non empty V67() set
bool [:X,ExtREAL:] is non empty set
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL f) + (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL (f + r) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
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 V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom r is Element of bool X
(dom f) /\ (dom r) is Element of bool X
f + r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f + r)) is ext-real Element of ExtREAL
R_EAL (f + 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
Integral (M,(R_EAL (f + r))) is ext-real Element of ExtREAL
max+ (R_EAL (f + r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f + r)))) is ext-real Element of ExtREAL
max- (R_EAL (f + r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f + r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f + r))))) - (integral+ (M,(max- (R_EAL (f + r))))) is ext-real Element of ExtREAL
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL f) is Element of bool X
dom (R_EAL r) is Element of bool X
(dom (R_EAL f)) /\ (dom (R_EAL r)) is Element of bool X
(R_EAL f) + (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL f) + (R_EAL r))) is ext-real Element of ExtREAL
max+ ((R_EAL f) + (R_EAL r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL f) + (R_EAL r)))) is ext-real Element of ExtREAL
max- ((R_EAL f) + (R_EAL r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL f) + (R_EAL r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL f) + (R_EAL r))))) - (integral+ (M,(max- ((R_EAL f) + (R_EAL r))))) is ext-real Element of ExtREAL
B is Element of S
(R_EAL f) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL f) | B)) is ext-real Element of ExtREAL
max+ ((R_EAL f) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL f) | B))) is ext-real Element of ExtREAL
max- ((R_EAL f) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL f) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL f) | B)))) - (integral+ (M,(max- ((R_EAL f) | B)))) is ext-real Element of ExtREAL
(R_EAL r) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL r) | B)) is ext-real Element of ExtREAL
max+ ((R_EAL r) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL r) | B))) is ext-real Element of ExtREAL
max- ((R_EAL r) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL r) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL r) | B)))) - (integral+ (M,(max- ((R_EAL r) | B)))) is ext-real Element of ExtREAL
(Integral (M,((R_EAL f) | B))) + (Integral (M,((R_EAL r) | B))) is ext-real Element of ExtREAL
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
r | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(r | B)) is ext-real Element of ExtREAL
R_EAL (r | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (r | B))) is ext-real Element of ExtREAL
max+ (R_EAL (r | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (r | B)))) is ext-real Element of ExtREAL
max- (R_EAL (r | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (r | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (r | B))))) - (integral+ (M,(max- (R_EAL (r | B))))) is ext-real Element of ExtREAL
(X,S,M,(f | B)) + (X,S,M,(r | B)) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,f) is ext-real Element of ExtREAL
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
Integral (M,(R_EAL f)) is ext-real Element of ExtREAL
max+ (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL f))) is ext-real Element of ExtREAL
max- (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL f)))) - (integral+ (M,(max- (R_EAL f)))) is ext-real Element of ExtREAL
r is V24() real ext-real Element of REAL
r (#) f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(r (#) f)) is ext-real Element of ExtREAL
R_EAL (r (#) f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (r (#) f))) is ext-real Element of ExtREAL
max+ (R_EAL (r (#) f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (r (#) f)))) is ext-real Element of ExtREAL
max- (R_EAL (r (#) f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (r (#) f)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (r (#) f))))) - (integral+ (M,(max- (R_EAL (r (#) f))))) is ext-real Element of ExtREAL
R_EAL r is ext-real Element of ExtREAL
(R_EAL r) * (X,S,M,f) is ext-real Element of ExtREAL
r (#) (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(r (#) (R_EAL f))) is ext-real Element of ExtREAL
max+ (r (#) (R_EAL f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (r (#) (R_EAL f)))) is ext-real Element of ExtREAL
max- (r (#) (R_EAL f)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (r (#) (R_EAL f)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (r (#) (R_EAL f))))) - (integral+ (M,(max- (r (#) (R_EAL f))))) is ext-real Element of ExtREAL
(R_EAL r) * (Integral (M,(R_EAL 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
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
[:X,REAL:] is non empty V66() V67() V68() set
bool [:X,REAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is Element of S
f | r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | r)) is ext-real Element of ExtREAL
R_EAL (f | 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
Integral (M,(R_EAL (f | r))) is ext-real Element of ExtREAL
max+ (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | r)))) is ext-real Element of ExtREAL
max- (R_EAL (f | r)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | r)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | r))))) - (integral+ (M,(max- (R_EAL (f | r))))) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
f + r is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
dom (f + r) is Element of bool X
B is Element of S
(X,S,M,(f + r),B) is ext-real Element of ExtREAL
(f + r) | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,((f + r) | B)) is ext-real Element of ExtREAL
R_EAL ((f + r) | B) 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
Integral (M,(R_EAL ((f + r) | B))) is ext-real Element of ExtREAL
max+ (R_EAL ((f + r) | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL ((f + r) | B)))) is ext-real Element of ExtREAL
max- (R_EAL ((f + r) | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL ((f + r) | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL ((f + r) | B))))) - (integral+ (M,(max- (R_EAL ((f + r) | B))))) is ext-real Element of ExtREAL
(X,S,M,f,B) is ext-real Element of ExtREAL
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
(X,S,M,r,B) is ext-real Element of ExtREAL
r | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(r | B)) is ext-real Element of ExtREAL
R_EAL (r | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (r | B))) is ext-real Element of ExtREAL
max+ (R_EAL (r | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (r | B)))) is ext-real Element of ExtREAL
max- (R_EAL (r | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (r | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (r | B))))) - (integral+ (M,(max- (R_EAL (r | B))))) is ext-real Element of ExtREAL
(X,S,M,f,B) + (X,S,M,r,B) is ext-real Element of ExtREAL
R_EAL (f + r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom (R_EAL (f + r)) is Element of bool X
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
R_EAL r is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
(R_EAL f) + (R_EAL r) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
dom ((R_EAL f) + (R_EAL r)) is Element of bool X
Integral_on (M,B,((R_EAL f) + (R_EAL r))) is ext-real Element of ExtREAL
((R_EAL f) + (R_EAL r)) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(((R_EAL f) + (R_EAL r)) | B)) is ext-real Element of ExtREAL
max+ (((R_EAL f) + (R_EAL r)) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (((R_EAL f) + (R_EAL r)) | B))) is ext-real Element of ExtREAL
max- (((R_EAL f) + (R_EAL r)) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (((R_EAL f) + (R_EAL r)) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((R_EAL f) + (R_EAL r)) | B)))) - (integral+ (M,(max- (((R_EAL f) + (R_EAL r)) | B)))) is ext-real Element of ExtREAL
Integral_on (M,B,(R_EAL f)) is ext-real Element of ExtREAL
(R_EAL f) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL f) | B)) is ext-real Element of ExtREAL
max+ ((R_EAL f) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL f) | B))) is ext-real Element of ExtREAL
max- ((R_EAL f) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL f) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL f) | B)))) - (integral+ (M,(max- ((R_EAL f) | B)))) is ext-real Element of ExtREAL
Integral_on (M,B,(R_EAL r)) is ext-real Element of ExtREAL
(R_EAL r) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL r) | B)) is ext-real Element of ExtREAL
max+ ((R_EAL r) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL r) | B))) is ext-real Element of ExtREAL
max- ((R_EAL r) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL r) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL r) | B)))) - (integral+ (M,(max- ((R_EAL r) | B)))) is ext-real Element of ExtREAL
(Integral_on (M,B,(R_EAL f))) + (Integral_on (M,B,(R_EAL r))) 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)
[:S,ExtREAL:] is non empty V67() set
bool [:S,ExtREAL:] is non empty set
M is V7() V10(S) V11( ExtREAL ) Function-like V32(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
r is V24() real ext-real Element of REAL
r (#) f is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
R_EAL r is ext-real Element of ExtREAL
B is Element of S
f | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,(r (#) f),B) is ext-real Element of ExtREAL
(r (#) f) | B is V7() V10(X) V11( REAL ) Function-like V66() V67() V68() Element of bool [:X,REAL:]
(X,S,M,((r (#) f) | B)) is ext-real Element of ExtREAL
R_EAL ((r (#) f) | B) 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
Integral (M,(R_EAL ((r (#) f) | B))) is ext-real Element of ExtREAL
max+ (R_EAL ((r (#) f) | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL ((r (#) f) | B)))) is ext-real Element of ExtREAL
max- (R_EAL ((r (#) f) | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL ((r (#) f) | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL ((r (#) f) | B))))) - (integral+ (M,(max- (R_EAL ((r (#) f) | B))))) is ext-real Element of ExtREAL
(X,S,M,f,B) is ext-real Element of ExtREAL
(X,S,M,(f | B)) is ext-real Element of ExtREAL
R_EAL (f | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,(R_EAL (f | B))) is ext-real Element of ExtREAL
max+ (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL (f | B)))) is ext-real Element of ExtREAL
max- (R_EAL (f | B)) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL (f | B)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL (f | B))))) - (integral+ (M,(max- (R_EAL (f | B))))) is ext-real Element of ExtREAL
(R_EAL r) * (X,S,M,f,B) is ext-real Element of ExtREAL
R_EAL f is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
r (#) (R_EAL f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral_on (M,B,(r (#) (R_EAL f))) is ext-real Element of ExtREAL
(r (#) (R_EAL f)) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((r (#) (R_EAL f)) | B)) is ext-real Element of ExtREAL
max+ ((r (#) (R_EAL f)) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((r (#) (R_EAL f)) | B))) is ext-real Element of ExtREAL
max- ((r (#) (R_EAL f)) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((r (#) (R_EAL f)) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((r (#) (R_EAL f)) | B)))) - (integral+ (M,(max- ((r (#) (R_EAL f)) | B)))) is ext-real Element of ExtREAL
Integral_on (M,B,(R_EAL f)) is ext-real Element of ExtREAL
(R_EAL f) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL f) | B)) is ext-real Element of ExtREAL
max+ ((R_EAL f) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL f) | B))) is ext-real Element of ExtREAL
max- ((R_EAL f) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL f) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL f) | B)))) - (integral+ (M,(max- ((R_EAL f) | B)))) is ext-real Element of ExtREAL
(R_EAL r) * (Integral_on (M,B,(R_EAL f))) is ext-real Element of ExtREAL
R_EAL (r (#) f) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral_on (M,B,(R_EAL (r (#) f))) is ext-real Element of ExtREAL
(R_EAL (r (#) f)) | B is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
Integral (M,((R_EAL (r (#) f)) | B)) is ext-real Element of ExtREAL
max+ ((R_EAL (r (#) f)) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ ((R_EAL (r (#) f)) | B))) is ext-real Element of ExtREAL
max- ((R_EAL (r (#) f)) | B) is V7() V10(X) V11( ExtREAL ) Function-like V67() Element of bool [:X,ExtREAL:]
integral+ (M,(max- ((R_EAL (r (#) f)) | B))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((R_EAL (r (#) f)) | B)))) - (integral+ (M,(max- ((R_EAL (r (#) f)) | B)))) is ext-real Element of ExtREAL