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

{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

{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

f . c

- +infty is ext-real Element of ExtREAL

|.(f . c

c

rng c

bool S is non empty set

union (rng c

dom c

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

f . c

c

1 / (c

B - (1 / (c

R_EAL (B - (1 / (c

great_dom ((R_EAL r),(R_EAL (B - (1 / (c

S /\ (great_dom ((R_EAL r),(R_EAL (B - (1 / (c

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

f . c

c

1 / (c

B + (1 / (c

R_EAL (B + (1 / (c

less_dom ((R_EAL r),(R_EAL (B + (1 / (c

S /\ (less_dom ((R_EAL r),(R_EAL (B + (1 / (c

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

f . c

c

1 / (c

B - (1 / (c

R_EAL (B - (1 / (c

less_eq_dom ((R_EAL r),(R_EAL (B - (1 / (c

S /\ (less_eq_dom ((R_EAL r),(R_EAL (B - (1 / (c

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

f . c

c

1 / (c

B + (1 / (c

R_EAL (B + (1 / (c

great_eq_dom ((R_EAL r),(R_EAL (B + (1 / (c

S /\ (great_eq_dom ((R_EAL r),(R_EAL (B + (1 / (c

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

rng c

bool S is non empty set

union (rng c

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

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

F is V24() real ext-real rational set

c

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

|.(