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 (rng (F | (Seg (m + 1))))) is Element of K19(X)
dom (f | (union (rng (F | (Seg (m + 1)))))) is Element of K19(X)
x1 is Element of X
(f | (union (rng (F | (Seg m))))) . x1 is ext-real Element of ExtREAL
f . x1 is ext-real Element of ExtREAL
(f | (union (rng (F | (Seg (m + 1)))))) . x1 is ext-real 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)
(less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) \/ (F . (m + 1)) is set
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 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
f . x1 is ext-real Element of ExtREAL
(f | (union (rng (F | (Seg (m + 1)))))) . 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 (rng (F | (Seg (m + 1))))) is Element of K19(X)
dom (f | (union (rng (F | (Seg (m + 1)))))) is Element of K19(X)
x1 is Element of X
(f | (union (rng (F | (Seg m))))) . x1 is ext-real Element of ExtREAL
f . x1 is ext-real Element of ExtREAL
(f | (union (rng (F | (Seg (m + 1)))))) . x1 is ext-real Element of ExtREAL
(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)
x1 is Element of X
f . x1 is ext-real Element of ExtREAL
R_EAL r1 is ext-real Element of ExtREAL
y is ext-real Element of ExtREAL
(f | (union (rng (F | (Seg (m + 1)))))) . x1 is ext-real Element of ExtREAL
A /\ (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r))) is Element of K19(X)
A /\ (F . (m + 1)) is set
(A /\ (less_dom ((f | (union (rng (F | (Seg m))))),(R_EAL r)))) \/ (A /\ (F . (m + 1))) is set
r1 is V30() real ext-real Element of REAL
F . (m + 1) is set
Seg (len F) is V37() V44( len F) V66() V67() V68() V69() V70() V71() Element of K19(NAT)
F | (Seg (len F)) is Relation-like NAT -defined S -valued Function-like FinSubsequence-like Element of K19(K20(NAT,S))
f | (dom f) is Relation-like X -defined ExtREAL -valued Function-like ext-real-valued Element of K19(K20(X,ExtREAL))