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
{ b1 where b1 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 : ( 1 <= b1 & b1 <= 1 ) } is set
{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
{ b1 where b1 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 : ( 1 <= b1 & b1 <= 2 ) } is set
{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