:: MESFUNC2 semantic presentation

REAL is non empty V37() V66() V67() V68() V72() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V37() V42() V43() V66() V67() V68() V69() V70() V71() V72() Element of K19(REAL)

K19(REAL) is V37() set

ExtREAL is non empty V67() set

K20(NAT,ExtREAL) is V37() ext-real-valued set

K19(K20(NAT,ExtREAL)) is V37() set

K19(ExtREAL) is set

{} is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() set

the functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() set is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() set

1 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

{{},1} is non empty V66() V67() V68() V69() V70() V71() set

INT is non empty V37() V66() V67() V68() V69() V70() V72() set

omega is non empty epsilon-transitive epsilon-connected ordinal V37() V42() V43() V66() V67() V68() V69() V70() V71() V72() set

K19(omega) is V37() set

K19(NAT) is V37() set

K20(NAT,REAL) is V37() complex-valued ext-real-valued real-valued set

K19(K20(NAT,REAL)) is V37() set

K19(K19(REAL)) is V37() set

COMPLEX is non empty V37() V66() V72() set

RAT is non empty V37() V66() V67() V68() V69() V72() set

K19(RAT) is V37() set

K20(COMPLEX,COMPLEX) is V37() complex-valued set

K19(K20(COMPLEX,COMPLEX)) is V37() set

K20(K20(COMPLEX,COMPLEX),COMPLEX) is V37() complex-valued set

K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is V37() set

K20(REAL,REAL) is V37() complex-valued ext-real-valued real-valued set

K19(K20(REAL,REAL)) is V37() set

K20(K20(REAL,REAL),REAL) is V37() complex-valued ext-real-valued real-valued set

K19(K20(K20(REAL,REAL),REAL)) is V37() set

K20(RAT,RAT) is RAT -valued V37() complex-valued ext-real-valued real-valued set

K19(K20(RAT,RAT)) is V37() set

K20(K20(RAT,RAT),RAT) is RAT -valued V37() complex-valued ext-real-valued real-valued set

K19(K20(K20(RAT,RAT),RAT)) is V37() set

K20(INT,INT) is RAT -valued INT -valued V37() complex-valued ext-real-valued real-valued set

K19(K20(INT,INT)) is V37() set

K20(K20(INT,INT),INT) is RAT -valued INT -valued V37() complex-valued ext-real-valued real-valued set

K19(K20(K20(INT,INT),INT)) is V37() set

K20(NAT,NAT) is RAT -valued INT -valued V37() complex-valued ext-real-valued real-valued natural-valued set

K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued V37() complex-valued ext-real-valued real-valued natural-valued set

K19(K20(K20(NAT,NAT),NAT)) is V37() set

2 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

3 is non empty epsilon-transitive epsilon-connected ordinal natural V30() real ext-real positive non negative V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V35() rational V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() Element of NAT

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

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

{-infty} is non empty V12() V44(1) V67() set

{+infty} is non empty V12() V44(1) V67() set

1. is ext-real Element of ExtREAL

union {} is epsilon-transitive epsilon-connected ordinal set

dom {} is set

rng {} is set

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

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

K245(-infty) is non empty ext-real positive non negative set

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

S is Element of X

f . S is ext-real Element of ExtREAL

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

rng f is V67() Element of K19(ExtREAL)

S is set

dom f is set

f . S is ext-real set

A is Element of X

f . A is ext-real Element of ExtREAL

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

1 (#) f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

dom (1 (#) f) is Element of K19(X)

S is Element of X

f . S is ext-real Element of ExtREAL

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

R_EAL 1 is ext-real Element of ExtREAL

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

f + S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (f + S) is Element of K19(X)

dom S is Element of K19(X)

(dom f) /\ (dom S) is Element of K19(X)

f - S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (f - S) is Element of K19(X)

rng f is V67() Element of K19(ExtREAL)

f " {+infty} is Element of K19(X)

f " {-infty} is Element of K19(X)

S " {-infty} is Element of K19(X)

(f " {+infty}) /\ (S " {-infty}) is Element of K19(X)

S " {+infty} is Element of K19(X)

(f " {-infty}) /\ (S " {+infty}) is Element of K19(X)

((f " {+infty}) /\ (S " {-infty})) \/ ((f " {-infty}) /\ (S " {+infty})) is Element of K19(X)

(f " {+infty}) /\ (S " {+infty}) is Element of K19(X)

(f " {-infty}) /\ (S " {-infty}) is Element of K19(X)

((f " {+infty}) /\ (S " {+infty})) \/ ((f " {-infty}) /\ (S " {-infty})) is Element of K19(X)

((dom f) /\ (dom S)) \ {} is Element of K19(X)

rng S is V67() Element of K19(ExtREAL)

S " {+infty} is Element of K19(X)

S " {-infty} is Element of K19(X)

f " {+infty} is Element of K19(X)

(f " {+infty}) /\ (S " {-infty}) is Element of K19(X)

f " {-infty} is Element of K19(X)

(f " {-infty}) /\ (S " {+infty}) is Element of K19(X)

((f " {+infty}) /\ (S " {-infty})) \/ ((f " {-infty}) /\ (S " {+infty})) is Element of K19(X)

(f " {+infty}) /\ (S " {+infty}) is Element of K19(X)

(f " {-infty}) /\ (S " {-infty}) is Element of K19(X)

((f " {+infty}) /\ (S " {+infty})) \/ ((f " {-infty}) /\ (S " {-infty})) is Element of K19(X)

((dom f) /\ (dom S)) \ {} is Element of K19(X)

X is non empty set

K19(X) is set

K19(K19(X)) is set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

K20(RAT,f) is V37() set

K19(K20(RAT,f)) is V37() set

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S + A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

F is Relation-like RAT -defined f -valued Function-like non empty total V25( RAT ,f) Element of K19(K20(RAT,f))

rng F is Element of K19(f)

K19(f) is set

union (rng F) is set

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_dom ((S + A),(R_EAL F)) is Element of K19(X)

m is Element of f

m /\ (less_dom ((S + A),(R_EAL F))) is Element of K19(X)

dom (S + A) is Element of K19(X)

dom S is Element of K19(X)

dom A is Element of K19(X)

(dom S) /\ (dom A) is Element of K19(X)

m is set

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

r is Element of X

S . r is ext-real Element of ExtREAL

A . r is ext-real Element of ExtREAL

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

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

|.(A . r).| is ext-real Element of ExtREAL

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

(R_EAL F) - (A . r) is ext-real Element of ExtREAL

K245((A . r)) is ext-real set

K244((R_EAL F),K245((A . r))) is ext-real set

F1 is V30() real ext-real Element of REAL

F - F1 is V30() real ext-real Element of REAL

G1 is V30() real ext-real Element of REAL

x is V30() real ext-real rational set

F - x is V30() real ext-real Element of REAL

R_EAL x is ext-real Element of ExtREAL

less_dom (S,(R_EAL x)) is Element of K19(X)

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

less_dom (A,(R_EAL (F - x))) is Element of K19(X)

m /\ (less_dom (S,(R_EAL x))) is Element of K19(X)

m /\ (less_dom (A,(R_EAL (F - x)))) is Element of K19(X)

(m /\ (less_dom (S,(R_EAL x)))) /\ (m /\ (less_dom (A,(R_EAL (F - x))))) is Element of K19(X)

dom F is V66() V67() V68() V69() Element of K19(RAT)

F . x is set

m is set

r is set

dom F is V66() V67() V68() V69() Element of K19(RAT)

G1 is set

F . G1 is set

F1 is V30() real ext-real rational set

R_EAL F1 is ext-real Element of ExtREAL

less_dom (S,(R_EAL F1)) is Element of K19(X)

m /\ (less_dom (S,(R_EAL F1))) is Element of K19(X)

F - F1 is V30() real ext-real Element of REAL

R_EAL (F - F1) is ext-real Element of ExtREAL

less_dom (A,(R_EAL (F - F1))) is Element of K19(X)

m /\ (less_dom (A,(R_EAL (F - F1)))) is Element of K19(X)

(m /\ (less_dom (S,(R_EAL F1)))) /\ (m /\ (less_dom (A,(R_EAL (F - F1))))) is Element of K19(X)

x is Element of X

A . x is ext-real Element of ExtREAL

S . x is ext-real Element of ExtREAL

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

|.(A . x).| is ext-real Element of ExtREAL

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

r1 is V30() real ext-real Element of REAL

x1 is V30() real ext-real Element of REAL

F - x1 is V30() real ext-real Element of REAL

r1 + x1 is V30() real ext-real Element of REAL

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

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

K20(NAT,RAT) is RAT -valued V37() complex-valued ext-real-valued real-valued set

K19(K20(NAT,RAT)) is V37() set

X is Relation-like Function-like set

dom X is set

rng X is set

X is non empty set

S is non empty set

K20(X,S) is set

K19(K20(X,S)) is set

f is non empty set

K20(f,S) is set

K19(K20(f,S)) is set

A is Relation-like X -defined S -valued Function-like non empty total V25(X,S) Element of K19(K20(X,S))

rng A is Element of K19(S)

K19(S) is set

F is Relation-like Function-like set

dom F is set

rng F is set

K20(f,X) is set

K19(K20(f,X)) is set

F is Relation-like f -defined X -valued Function-like non empty total V25(f,X) Element of K19(K20(f,X))

A * F is Relation-like f -defined S -valued Function-like non empty total V25(f,S) Element of K19(K20(f,S))

dom A is Element of K19(X)

K19(X) is set

m is Relation-like f -defined S -valued Function-like non empty total V25(f,S) Element of K19(K20(f,S))

dom m is Element of K19(f)

K19(f) is set

rng m is Element of K19(S)

m is Element of S

r is set

A . r is set

rng F is Element of K19(X)

F " is Relation-like Function-like set

dom (F ") is set

(F ") . r is set

rng (F ") is set

m . ((F ") . r) is set

F . ((F ") . r) is set

A . (F . ((F ") . r)) is set

m is Element of S

r is set

m . r is set

F " is Relation-like Function-like set

rng (F ") is set

dom (F ") is set

G1 is set

(F ") . G1 is set

rng F is Element of K19(X)

A . G1 is set

F . r is set

X is non empty set

K19(X) is set

K19(K19(X)) is set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is V30() real ext-real Element of REAL

S is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

K20(RAT,S) is V37() set

K19(K20(RAT,S)) is V37() set

A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

F is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

F is Element of S

m is set

m is V30() real ext-real rational set

R_EAL m is ext-real Element of ExtREAL

less_dom (A,(R_EAL m)) is Element of K19(X)

F /\ (less_dom (A,(R_EAL m))) is Element of K19(X)

f - m is V30() real ext-real Element of REAL

R_EAL (f - m) is ext-real Element of ExtREAL

less_dom (F,(R_EAL (f - m))) is Element of K19(X)

F /\ (less_dom (F,(R_EAL (f - m)))) is Element of K19(X)

(F /\ (less_dom (A,(R_EAL m)))) /\ (F /\ (less_dom (F,(R_EAL (f - m))))) is Element of K19(X)

m is Relation-like RAT -defined S -valued Function-like non empty total V25( RAT ,S) Element of K19(K20(RAT,S))

m is V30() real ext-real rational set

m . m is set

R_EAL m is ext-real Element of ExtREAL

less_dom (A,(R_EAL m)) is Element of K19(X)

F /\ (less_dom (A,(R_EAL m))) is Element of K19(X)

f - m is V30() real ext-real Element of REAL

R_EAL (f - m) is ext-real Element of ExtREAL

less_dom (F,(R_EAL (f - m))) is Element of K19(X)

F /\ (less_dom (F,(R_EAL (f - m)))) is Element of K19(X)

(F /\ (less_dom (A,(R_EAL m)))) /\ (F /\ (less_dom (F,(R_EAL (f - m))))) is Element of K19(X)

r is V30() real ext-real rational set

R_EAL r is ext-real Element of ExtREAL

less_dom (A,(R_EAL r)) is Element of K19(X)

F /\ (less_dom (A,(R_EAL r))) is Element of K19(X)

f - r is V30() real ext-real Element of REAL

R_EAL (f - r) is ext-real Element of ExtREAL

less_dom (F,(R_EAL (f - r))) is Element of K19(X)

F /\ (less_dom (F,(R_EAL (f - r)))) is Element of K19(X)

(F /\ (less_dom (A,(R_EAL r)))) /\ (F /\ (less_dom (F,(R_EAL (f - r))))) is Element of K19(X)

m is V30() real ext-real rational set

m . m is set

R_EAL m is ext-real Element of ExtREAL

less_dom (A,(R_EAL m)) is Element of K19(X)

F /\ (less_dom (A,(R_EAL m))) is Element of K19(X)

f - m is V30() real ext-real Element of REAL

R_EAL (f - m) is ext-real Element of ExtREAL

less_dom (F,(R_EAL (f - m))) is Element of K19(X)

F /\ (less_dom (F,(R_EAL (f - m)))) is Element of K19(X)

(F /\ (less_dom (A,(R_EAL m)))) /\ (F /\ (less_dom (F,(R_EAL (f - m))))) is Element of K19(X)

X is non empty set

K19(X) is set

K19(K19(X)) is set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S + A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

F is Element of f

F is V30() real ext-real set

R_EAL F is ext-real Element of ExtREAL

less_dom ((S + A),(R_EAL F)) is Element of K19(X)

F /\ (less_dom ((S + A),(R_EAL F))) is Element of K19(X)

K20(RAT,f) is V37() set

K19(K20(RAT,f)) is V37() set

m is V30() real ext-real Element of REAL

m is Relation-like RAT -defined f -valued Function-like non empty total V25( RAT ,f) Element of K19(K20(RAT,f))

K20(NAT,f) is V37() set

K19(K20(NAT,f)) is V37() set

rng m is Element of K19(f)

K19(f) is set

r is Relation-like NAT -defined f -valued Function-like non empty total V25( NAT ,f) Element of K19(K20(NAT,f))

rng r is non empty V54() M19(X,f)

R_EAL m is ext-real Element of ExtREAL

less_dom ((S + A),(R_EAL m)) is Element of K19(X)

F /\ (less_dom ((S + A),(R_EAL m))) is Element of K19(X)

union (rng r) is Element of f

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

f - S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

- S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

f + (- S) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (f - S) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom S is Element of K19(X)

(dom f) /\ (dom S) is Element of K19(X)

f " {+infty} is Element of K19(X)

S " {+infty} is Element of K19(X)

(f " {+infty}) /\ (S " {+infty}) is Element of K19(X)

f " {-infty} is Element of K19(X)

S " {-infty} is Element of K19(X)

(f " {-infty}) /\ (S " {-infty}) is Element of K19(X)

((f " {+infty}) /\ (S " {+infty})) \/ ((f " {-infty}) /\ (S " {-infty})) is Element of K19(X)

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

(- S) " {-infty} is Element of K19(X)

A is Element of X

S . A is ext-real Element of ExtREAL

dom (- S) is Element of K19(X)

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

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

A is Element of X

dom (- S) is Element of K19(X)

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

S . A is ext-real Element of ExtREAL

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

(- S) " {+infty} is Element of K19(X)

A is Element of X

S . A is ext-real Element of ExtREAL

dom (- S) is Element of K19(X)

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

A is Element of X

dom (- S) is Element of K19(X)

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

S . A is ext-real Element of ExtREAL

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

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

dom (f + (- S)) is Element of K19(X)

dom (- S) is Element of K19(X)

(dom f) /\ (dom (- S)) is Element of K19(X)

(f " {-infty}) /\ ((- S) " {+infty}) is Element of K19(X)

(f " {+infty}) /\ ((- S) " {-infty}) is Element of K19(X)

((f " {-infty}) /\ ((- S) " {+infty})) \/ ((f " {+infty}) /\ ((- S) " {-infty})) is Element of K19(X)

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

((f " {-infty}) /\ (S " {-infty})) \/ ((f " {+infty}) /\ (S " {+infty})) is Element of K19(X)

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

A is Element of X

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

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

f . A is ext-real Element of ExtREAL

S . A is ext-real Element of ExtREAL

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

K245((S . A)) is ext-real set

K244((f . A),K245((S . A))) is ext-real set

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

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

- 1 is V30() real ext-real non positive rational Element of REAL

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

- f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(- 1) (#) f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (- f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom ((- 1) (#) f) is Element of K19(X)

S is Element of X

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

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

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

f . S is ext-real Element of ExtREAL

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

R_EAL 1 is ext-real Element of ExtREAL

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

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

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

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is V30() real ext-real Element of REAL

S (#) f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (S (#) f) is Element of K19(X)

K19(X) is set

A is Element of X

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

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

dom f is Element of K19(X)

f . A is ext-real Element of ExtREAL

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

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

F is V30() real ext-real Element of REAL

S * F is V30() real ext-real Element of REAL

R_EAL (S * F) is ext-real Element of ExtREAL

R_EAL S is ext-real Element of ExtREAL

R_EAL F is ext-real Element of ExtREAL

(R_EAL S) * (R_EAL F) is ext-real Element of ExtREAL

X is non empty set

K19(X) is set

K19(K19(X)) is set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom A is Element of K19(X)

S - A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

F is Element of f

(- 1) (#) A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

- A is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S + (- A) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

0. is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL

dom f is Element of K19(X)

K19(X) is set

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom S is Element of K19(X)

A is set

A is set

A is Element of X

S . A is ext-real Element of ExtREAL

f . A is ext-real Element of ExtREAL

max ((f . A),0.) is ext-real Element of ExtREAL

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom S is Element of K19(X)

A is set

A is set

A is Element of X

S . A is ext-real Element of ExtREAL

f . A is ext-real Element of ExtREAL

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

max ((- (f . A)),0.) is ext-real Element of ExtREAL

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

f . S is ext-real Element of ExtREAL

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

f . S is ext-real Element of ExtREAL

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

- f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,(- f)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom (- f) is Element of K19(X)

dom (X,(- f)) is Element of K19(X)

S is Element of X

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

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

f . S is ext-real Element of ExtREAL

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

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom (X,f) is Element of K19(X)

f . S is ext-real Element of ExtREAL

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

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom (X,f) is Element of K19(X)

f . S is ext-real Element of ExtREAL

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

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

- 0. is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL

K134(0.) is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() set

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) - (X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom ((X,f) - (X,f)) is Element of K19(X)

(X,f) + (X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom ((X,f) + (X,f)) is Element of K19(X)

dom (X,f) is Element of K19(X)

dom (X,f) is Element of K19(X)

(X,f) " {+infty} is Element of K19(X)

(X,f) " {+infty} is Element of K19(X)

S is set

A is Element of X

(X,f) . A is ext-real Element of ExtREAL

(X,f) . A is ext-real Element of ExtREAL

((X,f) " {+infty}) /\ ((X,f) " {+infty}) is Element of K19(X)

(X,f) " {-infty} is Element of K19(X)

(X,f) " {-infty} is Element of K19(X)

S is set

A is Element of X

(X,f) . A is ext-real Element of ExtREAL

((X,f) " {-infty}) /\ ((X,f) " {-infty}) is Element of K19(X)

S is set

A is Element of X

(X,f) . A is ext-real Element of ExtREAL

((X,f) " {+infty}) /\ ((X,f) " {-infty}) is Element of K19(X)

S is set

A is Element of X

(X,f) . A is ext-real Element of ExtREAL

((X,f) " {-infty}) /\ ((X,f) " {+infty}) is Element of K19(X)

(dom f) /\ (dom f) is Element of K19(X)

{} \/ {} is V66() V67() V68() V69() V70() V71() set

((dom f) /\ (dom f)) \ ({} \/ {}) is Element of K19(X)

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

f . S is ext-real Element of ExtREAL

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

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom (X,f) is Element of K19(X)

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

f . S is ext-real Element of ExtREAL

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom (X,f) is Element of K19(X)

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

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

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

f . S is ext-real Element of ExtREAL

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

dom (X,f) is Element of K19(X)

dom (X,f) is Element of K19(X)

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

f . S is ext-real Element of ExtREAL

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

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

dom (X,f) is Element of K19(X)

K19(X) is set

dom f is Element of K19(X)

dom (X,f) is Element of K19(X)

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

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

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

- 0. is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL

K134(0.) is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() set

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is Element of X

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

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

f . S is ext-real Element of ExtREAL

dom (X,f) is Element of K19(X)

dom (X,f) is Element of K19(X)

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

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

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

- 0. is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() Element of ExtREAL

K134(0.) is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() set

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) - (X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

dom ((X,f) - (X,f)) is Element of K19(X)

S is Element of X

f . S is ext-real Element of ExtREAL

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

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

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

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

K245(((X,f) . S)) is ext-real set

K244(((X,f) . S),K245(((X,f) . S))) is ext-real set

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

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

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

|.f.| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) + (X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

K19(X) is set

dom ((X,f) + (X,f)) is Element of K19(X)

dom |.f.| is Element of K19(X)

S is Element of X

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

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

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

f . S is ext-real Element of ExtREAL

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

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

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

dom (X,f) is Element of K19(X)

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

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

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

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

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

f . S is ext-real Element of ExtREAL

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

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

dom (X,f) is Element of K19(X)

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

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

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

f . S is ext-real Element of ExtREAL

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

K19(X) is set

K19(K19(X)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

A is Element of S

F is V30() real ext-real set

R_EAL F is ext-real Element of ExtREAL

less_dom ((X,f),(R_EAL F)) is Element of K19(X)

A /\ (less_dom ((X,f),(R_EAL F))) is Element of K19(X)

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_dom ((X,f),(R_EAL F)) is Element of K19(X)

less_dom (f,(R_EAL F)) is Element of K19(X)

m is set

dom (X,f) is Element of K19(X)

(X,f) . m is ext-real Element of ExtREAL

m is Element of X

f . m is ext-real Element of ExtREAL

max ((f . m),0.) is ext-real Element of ExtREAL

dom f is Element of K19(X)

m is set

dom f is Element of K19(X)

f . m is ext-real Element of ExtREAL

m is Element of X

dom (X,f) is Element of K19(X)

f . m is ext-real Element of ExtREAL

max ((f . m),0.) is ext-real Element of ExtREAL

(X,f) . m is ext-real Element of ExtREAL

f . m is ext-real Element of ExtREAL

max ((f . m),0.) is ext-real Element of ExtREAL

(X,f) . m is ext-real Element of ExtREAL

f . m is ext-real Element of ExtREAL

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_dom ((X,f),(R_EAL F)) is Element of K19(X)

m is Element of X

dom (X,f) is Element of K19(X)

(X,f) . m is ext-real Element of ExtREAL

f . m is ext-real Element of ExtREAL

max ((f . m),0.) is ext-real Element of ExtREAL

F is V30() real ext-real Element of REAL

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

K19(X) is set

K19(K19(X)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom f is Element of K19(X)

(X,f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

A is Element of S

F is V30() real ext-real set

R_EAL F is ext-real Element of ExtREAL

less_dom ((X,f),(R_EAL F)) is Element of K19(X)

A /\ (less_dom ((X,f),(R_EAL F))) is Element of K19(X)

F is V30() real ext-real Element of REAL

(- 1) (#) f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

- f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

R_EAL F is ext-real Element of ExtREAL

less_dom ((X,f),(R_EAL F)) is Element of K19(X)

less_dom ((- f),(R_EAL F)) is Element of K19(X)

m is set

dom (X,f) is Element of K19(X)

(X,f) . m is ext-real Element of ExtREAL

m is Element of X

f . m is ext-real Element of ExtREAL

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

max ((- (f . m)),0.) is ext-real Element of ExtREAL

dom (- f) is Element of K19(X)

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

m is set

dom (- f) is Element of K19(X)

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

m is Element of X

dom (X,f) is Element of K19(X)

f . m is ext-real Element of ExtREAL

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

max ((- (f . m)),0.) is ext-real Element of ExtREAL

(X,f) . m is ext-real Element of ExtREAL

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

f . m is ext-real Element of ExtREAL

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

max ((- (f . m)),0.) is ext-real Element of ExtREAL

(X,f) . m is ext-real Element of ExtREAL

f . m is ext-real Element of ExtREAL

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

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_dom ((X,f),(R_EAL F)) is Element of K19(X)

m is Element of X

dom (X,f) is Element of K19(X)

(X,f) . m is ext-real Element of ExtREAL

f . m is ext-real Element of ExtREAL

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

max ((- (f . m)),0.) is ext-real Element of ExtREAL

F is V30() real ext-real Element of REAL

X is non empty set

K19(X) is set

K19(K19(X)) is set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom S is Element of K19(X)

|.S.| is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

A is Element of f

F is V30() real ext-real set

R_EAL F is ext-real Element of ExtREAL

less_dom (|.S.|,(R_EAL F)) is Element of K19(X)

A /\ (less_dom (|.S.|,(R_EAL F))) is Element of K19(X)

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_dom (|.S.|,(R_EAL F)) is Element of K19(X)

less_dom (S,(R_EAL F)) is Element of K19(X)

- F is V30() real ext-real Element of REAL

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

great_dom (S,(R_EAL (- F))) is Element of K19(X)

(less_dom (S,(R_EAL F))) /\ (great_dom (S,(R_EAL (- F)))) is Element of K19(X)

m is set

dom |.S.| is Element of K19(X)

|.S.| . m is ext-real Element of ExtREAL

m is Element of X

S . m is ext-real Element of ExtREAL

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

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

m is set

S . m is ext-real Element of ExtREAL

m is Element of X

dom |.S.| is Element of K19(X)

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

S . m is ext-real Element of ExtREAL

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

|.S.| . m is ext-real Element of ExtREAL

A /\ (great_dom (S,(R_EAL (- F)))) is Element of K19(X)

(A /\ (great_dom (S,(R_EAL (- F))))) /\ (less_dom (S,(R_EAL F))) is Element of K19(X)

X is set

f is set

chi (X,f) is Relation-like Function-like set

K20(f,ExtREAL) is ext-real-valued set

K19(K20(f,ExtREAL)) is set

S is set

chi (X,f) is Relation-like f -defined {{},1} -valued INT -valued Function-like total V25(f,{{},1}) complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(f,{{},1}))

K20(f,{{},1}) is INT -valued RAT -valued complex-valued ext-real-valued real-valued natural-valued set

K19(K20(f,{{},1})) is set

rng (chi (X,f)) is V66() V67() V68() V69() V70() V71() Element of K19({{},1})

K19({{},1}) is set

dom (chi (X,f)) is Element of K19(f)

K19(f) is set

X is non empty set

K19(X) is set

K19(K19(X)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is Element of f

(S,X) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

dom (S,X) is Element of K19(X)

A is Element of X

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

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

X is non empty set

K19(X) is set

K19(K19(X)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is Element of f

(S,X) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

A is Element of f

F is V30() real ext-real set

R_EAL F is ext-real Element of ExtREAL

less_eq_dom ((S,X),(R_EAL F)) is Element of K19(X)

A /\ (less_eq_dom ((S,X),(R_EAL F))) is Element of K19(X)

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_eq_dom ((S,X),(R_EAL F)) is Element of K19(X)

m is set

dom (S,X) is Element of K19(X)

m is Element of X

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

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_eq_dom ((S,X),(R_EAL F)) is Element of K19(X)

X \ S is Element of K19(X)

m is set

m is Element of X

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

m is set

m is Element of X

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

dom (S,X) is Element of K19(X)

F is V30() real ext-real Element of REAL

R_EAL F is ext-real Element of ExtREAL

less_eq_dom ((S,X),(R_EAL F)) is Element of K19(X)

m is Element of X

m is Element of X

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

F is V30() real ext-real Element of REAL

X is set

K19(X) is set

K19(K19(X)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

Seg 1 is non empty V12() V37() V44(1) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

K20((Seg 1),f) is set

K19(K20((Seg 1),f)) is set

S is Element of f

(Seg 1) --> S is Relation-like Seg 1 -defined f -valued Function-like non empty total V25( Seg 1,f) Element of K19(K20((Seg 1),f))

A is Relation-like Seg 1 -defined f -valued Function-like non empty total V25( Seg 1,f) Element of K19(K20((Seg 1),f))

dom A is V66() V67() V68() V69() V70() V71() Element of K19((Seg 1))

K19((Seg 1)) is set

F is Relation-like NAT -defined Function-like V37() FinSequence-like FinSubsequence-like set

rng F is set

F is Relation-like NAT -defined f -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of f

m is set

m is set

F . m is set

F . m is set

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

X is set

K19(X) is set

K19(K19(X)) is set

X is non empty set

K19(X) is set

K19(K19(X)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

K20(NAT,f) is V37() set

K19(K20(NAT,f)) is V37() set

S is Relation-like Function-like set

rng S is set

union (rng S) is set

dom S is set

A is set

S . A is set

F is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

S . F is set

F is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

F is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

A is Relation-like NAT -defined f -valued Function-like non empty total V25( NAT ,f) Element of K19(K20(NAT,f))

F is set

F is set

A . F is set

A . F is set

S . F is set

S . F is set

dom A is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F is Relation-like NAT -defined f -valued Function-like non empty total V25( NAT ,f) disjoint_valued Element of K19(K20(NAT,f))

rng F is non empty V54() M19(X,f)

union (rng F) is Element of f

F is set

m is set

m is set

S . m is set

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

S . r is set

F . r is Element of f

F is set

m is set

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

m is set

F . m is set

r is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

S . r is set

F . r is Element of f

F is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V37() V42() set

S . F is set

F . F is Element of f

F is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V37() V42() set

F . F is Element of f

X is non empty set

K19(X) is set

K19(K19(X)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is Relation-like Function-like set

rng S is set

union (rng S) is set

K20(NAT,f) is V37() set

K19(K20(NAT,f)) is V37() set

dom S is set

A is Relation-like NAT -defined f -valued Function-like non empty total V25( NAT ,f) disjoint_valued Element of K19(K20(NAT,f))

rng A is non empty V54() M19(X,f)

union (rng A) is Element of f

X is non empty set

K19(X) is set

K19(K19(X)) is set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

rng f is V67() Element of K19(ExtREAL)

S is set

dom f is Element of K19(X)

K19(X) is set

A is ext-real Element of ExtREAL

F is set

f . F is ext-real Element of ExtREAL

F is Element of X

f . F is ext-real Element of ExtREAL

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

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

X is non empty set

K19(X) is set

K19(K19(X)) is set

f is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

S is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V37() V42() set

Seg S is V37() V44(S) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

A is Relation-like set

A | (Seg S) is Relation-like set

F is Relation-like NAT -defined f -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of f

m is set

m is set

F . m is set

F . m is set

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F is Relation-like NAT -defined f -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of f

F . m is set

F . m is set

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

X is non empty set

K20(X,ExtREAL) is ext-real-valued set

K19(K20(X,ExtREAL)) is set

K19(X) is set

K19(K19(X)) is set

f is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

S is non empty compl-closed sigma-multiplicative V62() V63() V64() sigma-additive Element of K19(K19(X))

A is Element of S

dom f is Element of K19(X)

F is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like disjoint_valued FinSequence of S

rng F is Element of K19(S)

K19(S) is set

union (rng F) is set

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S

len F is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

Seg 0 is functional empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V30() real ext-real non positive non negative V37() V42() V44( 0 ) V44( {} ) FinSequence-membered V66() V67() V68() V69() V70() V71() V72() Element of K19(NAT)

F | (Seg 0) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

K20(NAT,S) is V37() set

K19(K20(NAT,S)) is V37() set

rng (F | (Seg 0)) is Element of K19(S)

union (rng (F | (Seg 0))) is set

f | (union (rng (F | (Seg 0)))) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V37() V42() set

Seg m is V37() V44(m) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F | (Seg m) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

m is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S

len m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

rng m is Element of K19(S)

union (rng m) is set

f | (union (rng m)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (f | (union (rng m))) is Element of K19(X)

(dom f) /\ {} is V66() V67() V68() V69() V70() V71() Element of K19(X)

r is V30() real ext-real set

R_EAL r is ext-real Element of ExtREAL

less_dom ((f | (union (rng m))),(R_EAL r)) is Element of K19(X)

A /\ (less_dom ((f | (union (rng m))),(R_EAL r))) is Element of K19(X)

G1 is set

m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V37() V42() set

Seg m is V37() V44(m) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F | (Seg m) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

rng (F | (Seg m)) is Element of K19(S)

union (rng (F | (Seg m))) is set

f | (union (rng (F | (Seg m)))) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

m + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

Seg (m + 1) is V37() V44(m + 1) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F | (Seg (m + 1)) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

rng (F | (Seg (m + 1))) is Element of K19(S)

union (rng (F | (Seg (m + 1)))) is set

f | (union (rng (F | (Seg (m + 1))))) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

m is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

m + 1 is epsilon-transitive epsilon-connected ordinal natural V30() real ext-real V35() rational V37() V42() V66() V67() V68() V69() V70() V71() Element of NAT

Seg (m + 1) is V37() V44(m + 1) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F | (Seg (m + 1)) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

rng (F | (Seg (m + 1))) is Element of K19(S)

union (rng (F | (Seg (m + 1)))) is set

f | (union (rng (F | (Seg (m + 1))))) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

r is V30() real ext-real set

R_EAL r is ext-real Element of ExtREAL

less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r)) is Element of K19(X)

A /\ (less_dom ((f | (union (rng (F | (Seg (m + 1)))))),(R_EAL r))) is Element of K19(X)

F . (m + 1) is set

Seg m is V37() V44(m) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F | (Seg m) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

rng (F | (Seg m)) is Element of K19(S)

union (rng (F | (Seg m))) is set

f | (union (rng (F | (Seg m)))) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) is Element of K19(X)

Seg (len F) is V37() V44( len F) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

G1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S

<*{}*> is Relation-like NAT -defined Function-like non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like set

G1 ^ <*{}*> is Relation-like NAT -defined Function-like non empty V37() FinSequence-like FinSubsequence-like set

rng G1 is Element of K19(S)

rng <*{}*> is set

(rng G1) \/ (rng <*{}*>) is set

{{}} is non empty V12() V44(1) V66() V67() V68() V69() V70() V71() set

(rng G1) \/ {{}} is non empty set

union (rng G1) is set

union {{}} is set

(union (rng G1)) \/ (union {{}}) is set

(union (rng G1)) \/ {} is set

F . (m + 1) is set

Seg m is V37() V44(m) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

F | (Seg m) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))

Seg (len F) is V37() V44( len F) V66() V67() V68() V69() V70() V71() Element of K19(NAT)

dom F is V66() V67() V68() V69() V70() V71() Element of K19(NAT)

rng F is Element of K19(S)

F1 is Element of K19(X)

x is Element of X

G1 is Relation-like NAT -defined S -valued Function-like V37() FinSequence-like FinSubsequence-like FinSequence of S

<*(F . (m + 1))*> is Relation-like NAT -defined Function-like non empty V12() V37() V44(1) FinSequence-like FinSubsequence-like set

G1 ^ <*(F . (m + 1))*> is Relation-like NAT -defined Function-like non empty V37() FinSequence-like FinSubsequence-like set

rng G1 is Element of K19(S)

rng <*(F . (m + 1))*> is set

(rng G1) \/ (rng <*(F . (m + 1))*>) is set

{(F . (m + 1))} is non empty V12() V44(1) set

(rng G1) \/ {(F . (m + 1))} is non empty set

union (rng G1) is set

union {(F . (m + 1))} is set

(union (rng G1)) \/ (union {(F . (m + 1))}) is set

(union (rng G1)) \/ (F . (m + 1)) is set

f . x is ext-real Element of ExtREAL

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

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

r1 is V30() real ext-real Element of REAL

rng (F | (Seg m)) is Element of K19(S)

union (rng (F | (Seg m))) is set

f | (union (rng (F | (Seg m)))) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)) is Element of K19(X)

x1 is set

dom (f | (union (rng (F | (Seg (m + 1)))))) is Element of K19(X)

(dom f) /\ (union (rng (F | (Seg (m + 1))))) is Element of K19(X)

(dom f) /\ (union (rng G1)) is Element of K19(X)

(dom f) /\ (F . (m + 1)) is Element of K19(X)

((dom f) /\ (union (rng G1))) \/ ((dom f) /\ (F . (m + 1))) is Element of K19(X)

x1 is Element of X

(f | (union (rng (F | (Seg (m + 1)))))) . x1 is ext-real Element of ExtREAL

f . x1 is ext-real Element of ExtREAL

f | F1 is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (f | F1) is Element of K19(X)

(dom f) /\ F1 is Element of K19(X)

f | (union (rng G1)) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))

dom (f | (union (rng G1))) is Element of K19(X)

(f | (union (rng G1))) . x1 is ext-real Element of ExtREAL

x1 is set

dom (f | (union (rng (F | (Seg m))))) is Element of K19(X)

(dom f) /\ (union (rng G1)) is Element of K19(X)

(dom f) /\ (union (<