:: MESFUNC5 semantic presentation

REAL is non empty non trivial non finite complex-membered ext-real-membered real-membered V74() non bounded_below non bounded_above V120() set

NAT is epsilon-transitive epsilon-connected ordinal non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() left_end bounded_below Element of bool REAL

bool REAL is non empty set

ExtREAL is non empty ext-real-membered V120() set

[:NAT,ExtREAL:] is non empty V59() set

bool [:NAT,ExtREAL:] is non empty set

bool ExtREAL is non empty set

COMPLEX is non empty non trivial non finite complex-membered V74() set

omega is epsilon-transitive epsilon-connected ordinal non empty complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() left_end bounded_below set

bool omega is non empty set

bool NAT is non empty set

[:NAT,REAL:] is non empty V58() V59() V60() set

bool [:NAT,REAL:] is non empty set

RAT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered V74() set

INT is non empty non trivial non finite complex-membered ext-real-membered real-membered rational-membered integer-membered V74() set

{} is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set

the epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set

1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

{{},1} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

bool (bool REAL) is non empty set

bool RAT is non empty set

[:COMPLEX,COMPLEX:] is non empty V58() set

bool [:COMPLEX,COMPLEX:] is non empty set

[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V58() set

bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set

[:REAL,REAL:] is non empty V58() V59() V60() set

bool [:REAL,REAL:] is non empty set

[:[:REAL,REAL:],REAL:] is non empty V58() V59() V60() set

bool [:[:REAL,REAL:],REAL:] is non empty set

[:RAT,RAT:] is RAT -valued non empty V58() V59() V60() set

bool [:RAT,RAT:] is non empty set

[:[:RAT,RAT:],RAT:] is RAT -valued non empty V58() V59() V60() set

bool [:[:RAT,RAT:],RAT:] is non empty set

[:INT,INT:] is RAT -valued INT -valued non empty V58() V59() V60() set

bool [:INT,INT:] is non empty set

[:[:INT,INT:],INT:] is RAT -valued INT -valued non empty V58() V59() V60() set

bool [:[:INT,INT:],INT:] is non empty set

[:NAT,NAT:] is RAT -valued INT -valued non empty V58() V59() V60() V61() set

[:[:NAT,NAT:],NAT:] is RAT -valued INT -valued non empty V58() V59() V60() V61() set

bool [:[:NAT,NAT:],NAT:] is non empty set

K535() is set

2 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

3 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

0. is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() Element of ExtREAL

+infty is non empty non real ext-real positive non negative Element of ExtREAL

0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() Element of NAT

|.+infty.| is ext-real Element of ExtREAL

-infty is non empty non real ext-real non positive negative Element of ExtREAL

|.-infty.| is ext-real Element of ExtREAL

{-infty} is non empty finite ext-real-membered left_end right_end set

{+infty} is non empty finite ext-real-membered left_end right_end set

Seg 1 is non empty finite V44(1) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

{ b

{1} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

Seg 2 is non empty finite V44(2) complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded Element of bool NAT

{ b

{1,2} is non empty finite complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

- 1 is non empty complex real ext-real non positive negative integer rational Element of REAL

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

{+infty,-infty} is non empty finite ext-real-membered left_end right_end set

REAL \/ {+infty,-infty} is non empty ext-real-membered set

bool {} is non empty finite V41() set

{{}} is non empty finite V41() complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end right_end bounded_below bounded_above real-bounded set

len {} is V42() set

- -infty is non empty ext-real positive non negative set

X is ext-real Element of ExtREAL

S is ext-real Element of ExtREAL

X - S is ext-real Element of ExtREAL

- S is ext-real set

X + (- S) is ext-real set

|.(X - S).| is ext-real Element of ExtREAL

S - X is ext-real Element of ExtREAL

- X is ext-real set

S + (- X) is ext-real set

|.(S - X).| is ext-real Element of ExtREAL

- (X - S) is ext-real Element of ExtREAL

|.(- (X - S)).| is ext-real Element of ExtREAL

S is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

S - X is ext-real Element of ExtREAL

- X is ext-real set

S + (- X) is ext-real set

X - S is ext-real Element of ExtREAL

- S is ext-real set

X + (- S) is ext-real set

|.(X - S).| is ext-real Element of ExtREAL

- |.(X - S).| is ext-real Element of ExtREAL

- (X - S) is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

S is ext-real Element of ExtREAL

X - S is ext-real Element of ExtREAL

- S is ext-real set

X + (- S) is ext-real set

|.(X - S).| is ext-real Element of ExtREAL

M is complex real ext-real set

S - X is ext-real Element of ExtREAL

- X is ext-real set

S + (- X) is ext-real set

R_EAL M is ext-real Element of ExtREAL

X is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set

2 |^ X is complex real ext-real Element of REAL

(2 |^ X) * X is complex real ext-real Element of REAL

S is ext-real Element of ExtREAL

M is complex real ext-real Element of REAL

f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

2 |^ f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

M * (2 |^ f) is complex real ext-real Element of REAL

(M * (2 |^ f)) + 1 is complex real ext-real Element of REAL

[\((M * (2 |^ f)) + 1)/] is complex real ext-real integer rational set

((M * (2 |^ f)) + 1) - 1 is complex real ext-real Element of REAL

B is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

(2 |^ f) * f is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered bounded_below Element of NAT

((2 |^ f) * f) + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

x is complex real ext-real integer rational set

[\x/] is complex real ext-real integer rational set

B - 1 is complex real ext-real integer rational Element of REAL

(B - 1) / (2 |^ X) is complex real ext-real Element of REAL

B / (2 |^ X) is complex real ext-real Element of REAL

B - 1 is complex real ext-real integer rational Element of REAL

0 + 1 is epsilon-transitive epsilon-connected ordinal natural non empty complex real ext-real positive non negative integer rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered left_end bounded_below Element of NAT

S is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set

X is epsilon-transitive epsilon-connected ordinal natural complex real ext-real non negative integer rational set

2 |^ X is complex real ext-real Element of REAL

(2 |^ X) * X is complex real ext-real Element of REAL

S / (2 |^ X) is complex real ext-real Element of REAL

M is ext-real Element of ExtREAL

M is ext-real set

X is ext-real set

S is ext-real set

max (X,S) is ext-real set

M * (max (X,S)) is ext-real set

M * X is ext-real set

M * S is ext-real set

max ((M * X),(M * S)) is ext-real set

min (X,S) is ext-real set

M * (min (X,S)) is ext-real set

min ((M * X),(M * S)) is ext-real set

M is ext-real Element of ExtREAL

X is ext-real Element of ExtREAL

S is ext-real Element of ExtREAL

min (X,S) is ext-real set

M * (min (X,S)) is ext-real set

M * X is ext-real Element of ExtREAL

M * S is ext-real Element of ExtREAL

max ((M * X),(M * S)) is ext-real set

max (X,S) is ext-real set

M * (max (X,S)) is ext-real set

min ((M * X),(M * S)) is ext-real set

min ((M * S),(M * X)) is ext-real set

X is set

[:X,ExtREAL:] is V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

rng S is ext-real-membered Element of bool ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

S . M is ext-real Element of ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

S . M is ext-real Element of ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

M is ext-real Element of ExtREAL

rng S is ext-real-membered set

dom S is Element of bool X

bool X is non empty set

f is set

S . f is ext-real Element of ExtREAL

X is set

[:X,ExtREAL:] is V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom S is Element of bool X

bool X is non empty set

M is ext-real Element of ExtREAL

rng S is ext-real-membered set

rng S is ext-real-membered Element of bool ExtREAL

f is set

S . f is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

rng S is ext-real-membered Element of bool ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

S . M is ext-real Element of ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

S . M is ext-real Element of ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

dom S is Element of bool X

bool X is non empty set

M is set

S . M is ext-real Element of ExtREAL

rng S is ext-real-membered Element of bool ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

S . M is ext-real Element of ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

S . M is ext-real Element of ExtREAL

M is set

dom S is Element of bool X

bool X is non empty set

dom S is Element of bool X

bool X is non empty set

M is set

S . M is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom S is Element of bool X

bool X is non empty set

M is set

S . M is ext-real Element of ExtREAL

M is set

S . M is ext-real Element of ExtREAL

M is set

M is set

S . M is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom S is Element of bool X

bool X is non empty set

M is set

S . M is ext-real Element of ExtREAL

M is set

S . M is ext-real Element of ExtREAL

M is set

M is set

S . M is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is set

S . M is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is set

S . M is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

X is non empty set

bool X is non empty set

bool (bool X) is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is non empty compl-closed sigma-multiplicative V109() V110() V111() sigma-additive Element of bool (bool X)

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

rng M is ext-real-membered Element of bool ExtREAL

M " {+infty} is Element of bool X

f is set

M . f is ext-real Element of ExtREAL

M " {-infty} is Element of bool X

f is set

M . f is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is set

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M | S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

f is set

dom (M | S) is Element of bool X

bool X is non empty set

(M | S) . f is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

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

rng M is ext-real-membered Element of bool ExtREAL

M " {-infty} is Element of bool X

rng S is ext-real-membered Element of bool ExtREAL

S " {-infty} is Element of bool X

S " {+infty} is Element of bool X

(S " {+infty}) /\ (M " {-infty}) is Element of bool X

M " {+infty} is Element of bool X

(S " {-infty}) /\ (M " {+infty}) is Element of bool X

((S " {+infty}) /\ (M " {-infty})) \/ ((S " {-infty}) /\ (M " {+infty})) is Element of bool X

((dom S) /\ (dom M)) \ {} is Element of bool X

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S - M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

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

rng M is ext-real-membered Element of bool ExtREAL

M " {+infty} is Element of bool X

rng S is ext-real-membered Element of bool ExtREAL

S " {-infty} is Element of bool X

S " {+infty} is Element of bool X

(S " {+infty}) /\ (M " {+infty}) is Element of bool X

M " {-infty} is Element of bool X

(S " {-infty}) /\ (M " {-infty}) is Element of bool X

((S " {+infty}) /\ (M " {+infty})) \/ ((S " {-infty}) /\ (M " {-infty})) 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,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is non empty compl-closed sigma-multiplicative V109() V110() V111() sigma-additive Element of bool (bool X)

[:RAT,S:] is non empty set

bool [:RAT,S:] is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M + f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

c is Relation-like RAT -defined S -valued 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

B is complex real ext-real Element of REAL

R_EAL B is ext-real Element of ExtREAL

less_dom ((M + f),(R_EAL B)) is Element of bool X

x is Element of S

x /\ (less_dom ((M + f),(R_EAL B))) is Element of bool X

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

I1 is set

a is set

dom c is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT

f1 is set

c . f1 is set

E is complex real ext-real rational set

R_EAL E is ext-real Element of ExtREAL

less_dom (M,(R_EAL E)) is Element of bool X

x /\ (less_dom (M,(R_EAL E))) is Element of bool X

B - E is complex real ext-real Element of REAL

R_EAL (B - E) is ext-real Element of ExtREAL

less_dom (f,(R_EAL (B - E))) is Element of bool X

x /\ (less_dom (f,(R_EAL (B - E)))) is Element of bool X

(x /\ (less_dom (M,(R_EAL E)))) /\ (x /\ (less_dom (f,(R_EAL (B - E))))) is Element of bool X

x is Element of X

M . x is ext-real Element of ExtREAL

f . x is ext-real Element of ExtREAL

NFPG is complex real ext-real Element of REAL

B - NFPG is complex real ext-real Element of REAL

DFPG is complex real ext-real Element of REAL

DFPG + NFPG is complex real ext-real Element of REAL

(M + f) . x is ext-real Element of ExtREAL

(M . x) + (f . x) is ext-real Element of ExtREAL

I1 is set

(M + f) . I1 is ext-real Element of ExtREAL

a is Element of X

M . a is ext-real Element of ExtREAL

f . a is ext-real Element of ExtREAL

(M . a) + (f . a) is ext-real Element of ExtREAL

(R_EAL B) - (f . a) is ext-real Element of ExtREAL

- (f . a) is ext-real set

(R_EAL B) + (- (f . a)) is ext-real set

E is complex real ext-real Element of REAL

B - E is complex real ext-real Element of REAL

f1 is complex real ext-real Element of REAL

x is complex real ext-real rational set

B - x is complex real ext-real Element of REAL

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

less_dom (f,(R_EAL (B - x))) is Element of bool X

x /\ (less_dom (f,(R_EAL (B - x)))) is Element of bool X

dom c is complex-membered ext-real-membered real-membered rational-membered Element of bool RAT

c . x is set

R_EAL x is ext-real Element of ExtREAL

less_dom (M,(R_EAL x)) is Element of bool X

x /\ (less_dom (M,(R_EAL x))) is Element of bool X

(x /\ (less_dom (M,(R_EAL x)))) /\ (x /\ (less_dom (f,(R_EAL (B - x))))) is Element of bool X

X is non empty set

[:X,REAL:] is non empty V58() V59() V60() set

bool [:X,REAL:] is non empty set

S is Relation-like X -defined REAL -valued Function-like V58() V59() V60() Element of bool [:X,REAL:]

[:X,ExtREAL:] is non empty V59() 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,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is non empty compl-closed sigma-multiplicative V109() V110() V111() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V59() set

bool [:S,ExtREAL:] is non empty set

f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

c is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

f + c is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (f + c) is Element of bool X

B is set

(f + c) . B is ext-real Element of ExtREAL

f . B is ext-real Element of ExtREAL

c . B is ext-real Element of ExtREAL

(f . B) + (c . B) is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is complex real ext-real Element of REAL

M (#) S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (M (#) S) is Element of bool X

bool X is non empty set

B is set

(M (#) S) . B is ext-real Element of ExtREAL

S . B is ext-real Element of ExtREAL

R_EAL M is ext-real Element of ExtREAL

(R_EAL M) * (S . B) is ext-real Element of ExtREAL

c is set

S . c is ext-real Element of ExtREAL

R_EAL M is ext-real Element of ExtREAL

(R_EAL M) * (S . c) is ext-real Element of ExtREAL

(M (#) S) . c is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom S is Element of bool X

bool X is non empty set

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom M is Element of bool X

(dom S) /\ (dom M) is Element of bool X

S - M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

f is set

dom (S - M) is Element of bool X

S " {+infty} is Element of bool X

M " {+infty} is Element of bool X

(S " {+infty}) /\ (M " {+infty}) is Element of bool X

S " {-infty} is Element of bool X

M " {-infty} is Element of bool X

(S " {-infty}) /\ (M " {-infty}) is Element of bool X

((S " {+infty}) /\ (M " {+infty})) \/ ((S " {-infty}) /\ (M " {-infty})) is Element of bool X

((dom S) /\ (dom M)) \ (((S " {+infty}) /\ (M " {+infty})) \/ ((S " {-infty}) /\ (M " {-infty}))) is Element of bool X

S . f is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

(S . f) - (M . f) is ext-real Element of ExtREAL

- (M . f) is ext-real set

(S . f) + (- (M . f)) is ext-real set

(S - M) . 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,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is non empty compl-closed sigma-multiplicative V109() V110() V111() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V59() set

bool [:S,ExtREAL:] is non empty set

f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

|.f.| is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (max- f) is Element of bool X

c is set

(max- f) . c is ext-real Element of ExtREAL

dom (max+ f) is Element of bool X

c is set

(max+ f) . c is ext-real Element of ExtREAL

c is set

dom |.f.| is Element of bool X

|.f.| . c is ext-real Element of ExtREAL

f . c is ext-real Element of ExtREAL

|.(f . c).| is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

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

f is set

M . f is ext-real Element of ExtREAL

S . f is ext-real Element of ExtREAL

(S . f) + (M . f) is ext-real Element of ExtREAL

(S + M) . f is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(S + M) + f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom ((S + M) + f) 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

dom f is Element of bool X

((dom S) /\ (dom M)) /\ (dom f) is Element of bool X

dom (S + M) is Element of bool X

(dom (S + M)) /\ (dom f) is Element of bool X

c is set

((S + M) + f) . c is ext-real Element of ExtREAL

(S + M) . c is ext-real Element of ExtREAL

f . c is ext-real Element of ExtREAL

((S + M) . c) + (f . c) is ext-real Element of ExtREAL

S . c is ext-real Element of ExtREAL

M . c is ext-real Element of ExtREAL

(S . c) + (M . c) is ext-real Element of ExtREAL

((S . c) + (M . c)) + (f . c) is ext-real Element of ExtREAL

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ (S + M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(max+ (S + M)) + (max- S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom ((max+ (S + M)) + (max- S)) 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

max- (S + M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(max- (S + M)) + (max+ S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom ((max- (S + M)) + (max+ S)) is Element of bool X

max- M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

((max+ (S + M)) + (max- S)) + (max- M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (((max+ (S + M)) + (max- S)) + (max- M)) is Element of bool X

max+ M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

((max- (S + M)) + (max+ S)) + (max+ M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (((max- (S + M)) + (max+ S)) + (max+ M)) is Element of bool X

dom (S + M) is Element of bool X

dom (max- (S + M)) is Element of bool X

dom (max- S) is Element of bool X

dom (max+ S) is Element of bool X

dom (max+ M) is Element of bool X

dom (max- M) is Element of bool X

f is set

(max- S) . f is ext-real Element of ExtREAL

c is set

(max+ S) . c is ext-real Element of ExtREAL

B is set

(max+ M) . B is ext-real Element of ExtREAL

x is set

(max- M) . x is ext-real Element of ExtREAL

dom (max+ (S + M)) is Element of bool X

f is set

(max+ (S + M)) . f is ext-real Element of ExtREAL

c is set

(max- (S + M)) . c is ext-real Element of ExtREAL

(dom (max+ (S + M))) /\ (dom (max- S)) is Element of bool X

(dom (max- (S + M))) /\ (dom (max+ S)) 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

f is set

((max+ (S + M)) + (max- S)) . f is ext-real Element of ExtREAL

((max- (S + M)) + (max+ S)) . f is ext-real Element of ExtREAL

(max- S) . f is ext-real Element of ExtREAL

(max+ (S + M)) . f is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(max+ S) . f is ext-real Element of ExtREAL

(max- (S + M)) . f is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

f is set

((max+ (S + M)) + (max- S)) . f is ext-real Element of ExtREAL

c is set

((max- (S + M)) + (max+ S)) . c is ext-real Element of ExtREAL

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

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ (S + M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(max+ (S + M)) + (max- S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

((max+ (S + M)) + (max- S)) + (max- M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- (S + M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(max- (S + M)) + (max+ S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

((max- (S + M)) + (max+ S)) + (max+ M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

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

f is set

(max- M) . f is ext-real Element of ExtREAL

dom (max+ M) is Element of bool X

f is set

(max+ M) . f is ext-real Element of ExtREAL

dom (max- S) is Element of bool X

dom S is Element of bool X

dom (max+ (S + M)) is Element of bool X

f is set

(max+ (S + M)) . f is ext-real Element of ExtREAL

dom (max+ S) is Element of bool X

f is set

(max+ S) . f is ext-real Element of ExtREAL

dom M is Element of bool X

f is set

(max- S) . f is ext-real Element of ExtREAL

dom (((max+ (S + M)) + (max- S)) + (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

f is set

(max- (S + M)) . f is ext-real Element of ExtREAL

f is set

(((max+ (S + M)) + (max- S)) + (max- M)) . f is ext-real Element of ExtREAL

(((max- (S + M)) + (max+ S)) + (max+ M)) . f is ext-real Element of ExtREAL

(max+ M) . f is ext-real Element of ExtREAL

M . f is ext-real Element of ExtREAL

max ((M . f),0) is ext-real set

(max+ (S + M)) . f is ext-real Element of ExtREAL

(S + M) . f is ext-real Element of ExtREAL

max (((S + M) . f),0) is ext-real set

S . f is ext-real Element of ExtREAL

(S . f) + (M . f) is ext-real Element of ExtREAL

max (((S . f) + (M . f)),0) is ext-real set

(max+ S) . f is ext-real Element of ExtREAL

max ((S . f),0) is ext-real set

(max- (S + M)) . f is ext-real Element of ExtREAL

- ((S + M) . f) is ext-real Element of ExtREAL

max ((- ((S + M) . f)),0) is ext-real set

- ((S . f) + (M . f)) is ext-real Element of ExtREAL

max ((- ((S . f) + (M . f))),0) is ext-real set

- (S . f) is ext-real Element of ExtREAL

(max- S) . f is ext-real Element of ExtREAL

max ((- (S . f)),0) is ext-real set

(max- M) . f is ext-real Element of ExtREAL

- (M . f) is ext-real Element of ExtREAL

max ((- (M . f)),0) is ext-real set

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((S . f) + (M . f)) + 0 is ext-real set

(((S . f) + (M . f)) + 0) + 0 is ext-real set

R_EAL 0 is ext-real Element of ExtREAL

((S . f) + (M . f)) + (R_EAL 0) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

(R_EAL 0) + (S . f) is ext-real Element of ExtREAL

((R_EAL 0) + (S . f)) + (M . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

(R_EAL 0) + (S . f) is ext-real Element of ExtREAL

((R_EAL 0) + (S . f)) + (R_EAL 0) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((S . f) + (M . f)) + (R_EAL 0) is ext-real Element of ExtREAL

(((S . f) + (M . f)) + (R_EAL 0)) + (- (M . f)) is ext-real Element of ExtREAL

((S . f) + (M . f)) - (M . f) is ext-real Element of ExtREAL

- (M . f) is ext-real set

((S . f) + (M . f)) + (- (M . f)) is ext-real set

(M . f) - (M . f) is ext-real Element of ExtREAL

(M . f) + (- (M . f)) is ext-real set

(S . f) + ((M . f) - (M . f)) is ext-real Element of ExtREAL

(S . f) + (R_EAL 0) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

(R_EAL 0) + (R_EAL 0) is ext-real Element of ExtREAL

((R_EAL 0) + (R_EAL 0)) + (- (M . f)) is ext-real Element of ExtREAL

0 + (- (M . f)) is ext-real set

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

(- ((S . f) + (M . f))) + (S . f) is ext-real Element of ExtREAL

((- ((S . f) + (M . f))) + (S . f)) + (R_EAL 0) is ext-real Element of ExtREAL

(- (M . f)) - (S . f) is ext-real Element of ExtREAL

- (S . f) is ext-real set

(- (M . f)) + (- (S . f)) is ext-real set

((- (M . f)) - (S . f)) + (S . f) is ext-real Element of ExtREAL

(- (S . f)) + (S . f) is ext-real Element of ExtREAL

(- (M . f)) + ((- (S . f)) + (S . f)) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

(R_EAL 0) + (R_EAL 0) is ext-real Element of ExtREAL

((R_EAL 0) + (R_EAL 0)) + (M . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((S . f) + (M . f)) + (- (S . f)) is ext-real Element of ExtREAL

(((S . f) + (M . f)) + (- (S . f))) + (R_EAL 0) is ext-real Element of ExtREAL

(S . f) - (S . f) is ext-real Element of ExtREAL

- (S . f) is ext-real set

(S . f) + (- (S . f)) is ext-real set

(M . f) + ((S . f) - (S . f)) is ext-real Element of ExtREAL

(M . f) + 0 is ext-real set

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

(- ((S . f) + (M . f))) + (R_EAL 0) is ext-real Element of ExtREAL

((- ((S . f) + (M . f))) + (R_EAL 0)) + (M . f) is ext-real Element of ExtREAL

(- ((S . f) + (M . f))) + (M . f) is ext-real Element of ExtREAL

(- (S . f)) - (M . f) is ext-real Element of ExtREAL

- (M . f) is ext-real set

(- (S . f)) + (- (M . f)) is ext-real set

((- (S . f)) - (M . f)) + (M . f) is ext-real Element of ExtREAL

(- (M . f)) + (M . f) is ext-real Element of ExtREAL

(- (S . f)) + ((- (M . f)) + (M . f)) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

(R_EAL 0) + (- (S . f)) is ext-real Element of ExtREAL

((R_EAL 0) + (- (S . f))) + (R_EAL 0) is ext-real Element of ExtREAL

0 + (- (S . f)) is ext-real set

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

(R_EAL 0) + (- (S . f)) is ext-real Element of ExtREAL

((R_EAL 0) + (- (S . f))) + (- (M . f)) is ext-real Element of ExtREAL

(- (S . f)) - (M . f) is ext-real Element of ExtREAL

- (M . f) is ext-real set

(- (S . f)) + (- (M . f)) is ext-real set

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

(- ((S . f) + (M . f))) + (R_EAL 0) is ext-real Element of ExtREAL

((- ((S . f) + (M . f))) + (R_EAL 0)) + (R_EAL 0) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

((max+ (S + M)) . f) + ((max- S) . f) is ext-real Element of ExtREAL

(((max+ (S + M)) . f) + ((max- S) . f)) + ((max- M) . f) is ext-real Element of ExtREAL

((max- (S + M)) . f) + ((max+ S) . f) is ext-real Element of ExtREAL

(((max- (S + M)) . f) + ((max+ S) . f)) + ((max+ M) . f) is ext-real Element of ExtREAL

(dom (max+ (S + M))) /\ (dom (max- S)) is Element of bool X

((dom (max+ (S + M))) /\ (dom (max- S))) /\ (dom (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,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is complex real ext-real Element of REAL

M (#) S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ (M (#) S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M (#) (max+ S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- (M (#) S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M (#) (max- S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

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 ext-real Element of ExtREAL

(M (#) (max+ S)) . f is ext-real Element of ExtREAL

(M (#) S) . f is ext-real Element of ExtREAL

max (((M (#) S) . f),0) is ext-real set

R_EAL M is ext-real Element of ExtREAL

S . f is ext-real Element of ExtREAL

(R_EAL M) * (S . f) is ext-real Element of ExtREAL

max (((R_EAL M) * (S . f)),0) is ext-real set

(max+ S) . f is ext-real Element of ExtREAL

(R_EAL M) * ((max+ S) . f) is ext-real Element of ExtREAL

max ((S . f),0) is ext-real set

M * (max ((S . f),0)) is ext-real set

M * (S . f) is ext-real set

M * 0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set

M * 0 is complex real ext-real set

max ((M * (S . f)),(M * 0)) is 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 ext-real Element of ExtREAL

(M (#) (max- S)) . f is ext-real Element of ExtREAL

(M (#) S) . f is ext-real Element of ExtREAL

- ((M (#) S) . f) is ext-real Element of ExtREAL

max ((- ((M (#) S) . f)),0) is ext-real set

R_EAL M is ext-real Element of ExtREAL

S . f is ext-real Element of ExtREAL

(R_EAL M) * (S . f) is ext-real Element of ExtREAL

- ((R_EAL M) * (S . f)) is ext-real Element of ExtREAL

max ((- ((R_EAL M) * (S . f))),0) is ext-real set

(max- S) . f is ext-real Element of ExtREAL

(R_EAL M) * ((max- S) . f) is ext-real Element of ExtREAL

- (S . f) is ext-real Element of ExtREAL

max ((- (S . f)),0) is ext-real set

M * (max ((- (S . f)),0)) is ext-real set

M * (- (S . f)) is ext-real set

M * 0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set

M * 0 is complex real ext-real set

max ((M * (- (S . f))),(M * 0)) is ext-real set

M * (S . f) is ext-real set

- (M * (S . f)) is ext-real set

max ((- (M * (S . f))),(M * 0)) is ext-real set

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is complex real ext-real Element of REAL

- M is complex real ext-real Element of REAL

(- M) (#) S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ ((- M) (#) S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M (#) (max- S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- ((- M) (#) S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M (#) (max+ S) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

R_EAL M is ext-real Element of ExtREAL

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

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 ext-real Element of ExtREAL

(M (#) (max- S)) . f is ext-real Element of ExtREAL

((- M) (#) S) . f is ext-real Element of ExtREAL

max ((((- M) (#) S) . f),0) is ext-real set

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

S . f is ext-real Element of ExtREAL

(R_EAL (- M)) * (S . f) is ext-real Element of ExtREAL

max (((R_EAL (- M)) * (S . f)),0) is ext-real set

(R_EAL M) * (S . f) is ext-real Element of ExtREAL

- ((R_EAL M) * (S . f)) is ext-real Element of ExtREAL

max ((- ((R_EAL M) * (S . f))),0) is ext-real set

(max- S) . f is ext-real Element of ExtREAL

(R_EAL M) * ((max- S) . f) is ext-real Element of ExtREAL

- (S . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

max ((- (S . f)),(R_EAL 0)) is ext-real set

(R_EAL M) * (max ((- (S . f)),(R_EAL 0))) is ext-real set

(R_EAL M) * (- (S . f)) is ext-real Element of ExtREAL

(R_EAL M) * (R_EAL 0) is ext-real Element of ExtREAL

max (((R_EAL M) * (- (S . f))),((R_EAL M) * (R_EAL 0))) is ext-real set

M * 0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set

M * 0 is complex real ext-real set

max ((- ((R_EAL M) * (S . f))),(M * 0)) is 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 ext-real Element of ExtREAL

(M (#) (max+ S)) . f is ext-real Element of ExtREAL

((- M) (#) S) . f is ext-real Element of ExtREAL

- (((- M) (#) S) . f) is ext-real Element of ExtREAL

max ((- (((- M) (#) S) . f)),0) is ext-real set

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

S . f is ext-real Element of ExtREAL

(R_EAL (- M)) * (S . f) is ext-real Element of ExtREAL

- ((R_EAL (- M)) * (S . f)) is ext-real Element of ExtREAL

max ((- ((R_EAL (- M)) * (S . f))),0) is ext-real set

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

(- (- (R_EAL M))) * (S . f) is ext-real Element of ExtREAL

max (((- (- (R_EAL M))) * (S . f)),0) is ext-real set

(max+ S) . f is ext-real Element of ExtREAL

(R_EAL M) * ((max+ S) . f) is ext-real Element of ExtREAL

R_EAL 0 is ext-real Element of ExtREAL

max ((S . f),(R_EAL 0)) is ext-real set

(R_EAL M) * (max ((S . f),(R_EAL 0))) is ext-real set

(R_EAL M) * (S . f) is ext-real Element of ExtREAL

M * 0 is epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural empty complex real ext-real non positive non negative integer functional finite V41() FinSequence-membered rational complex-membered ext-real-membered real-membered rational-membered integer-membered natural-membered V74() bounded_below bounded_above real-bounded V120() set

M * 0 is complex real ext-real set

max (((R_EAL M) * (S . f)),(M * 0)) is ext-real set

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is set

S | M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max+ (S | M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(max+ S) | M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

max- (S | M) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(max- S) | M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (max+ (S | M)) is Element of bool X

bool X is non empty set

dom (S | M) is Element of bool X

dom S is Element of bool X

(dom S) /\ 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) is Element of bool X

f is Element of X

(max+ (S | M)) . f is ext-real Element of ExtREAL

((max+ S) | M) . f is ext-real Element of ExtREAL

(max+ S) . f is ext-real Element of ExtREAL

(S | M) . f is ext-real Element of ExtREAL

max (((S | M) . f),0) is ext-real set

S . f is ext-real Element of ExtREAL

max ((S . f),0) is ext-real set

dom (max- (S | 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) is Element of bool X

f is Element of X

(max- (S | M)) . f is ext-real Element of ExtREAL

((max- S) | M) . f is ext-real Element of ExtREAL

(max- S) . f is ext-real Element of ExtREAL

(S | M) . f is ext-real Element of ExtREAL

- ((S | M) . f) is ext-real Element of ExtREAL

max ((- ((S | M) . f)),0) is ext-real set

S . f is ext-real Element of ExtREAL

- (S . f) is ext-real Element of ExtREAL

max ((- (S . f)),0) is ext-real set

X is non empty set

[:X,ExtREAL:] is non empty V59() set

bool [:X,ExtREAL:] is non empty set

S is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

S + M is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom (S + M) is Element of bool X

bool X is non empty set

f is set

(S + M) | f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom ((S + M) | f) is Element of bool X

S | f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

M | f is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

(S | f) + (M | f) is Relation-like X -defined ExtREAL -valued Function-like V59() Element of bool [:X,ExtREAL:]

dom ((S | f) + (M | f)) is Element of bool X

dom M is Element of bool X