REAL is non empty V32() V58() V59() V60() V64() set
NAT is non empty V15() V16() V17() V58() V59() V60() V61() V62() V63() V64() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V59() set
[:NAT,ExtREAL:] is non empty set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
NAT is non empty V15() V16() V17() V58() V59() V60() V61() V62() V63() V64() set
bool NAT is non empty set
[:NAT,REAL:] is non empty set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
{} is empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V58() V59() V60() V61() V62() V63() V64() set
the empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V58() V59() V60() V61() V62() V63() V64() set is empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V58() V59() V60() V61() V62() V63() V64() set
0 is empty V15() V16() V17() V19() V20() V21() V22() ext-real non positive non negative V58() V59() V60() V61() V62() V63() V64() V92() Element of NAT
1 is non empty V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
0. is empty V15() V16() V17() V19() V20() V21() ext-real non positive non negative V58() V59() V60() V61() V62() V63() V64() Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty set
bool [:S,ExtREAL:] is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V29(S, ExtREAL ) V74() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
M * F is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
{{},{}} is non empty V58() V59() V60() V61() V62() V63() set
{{}} is non empty V58() V59() V60() V61() V62() V63() set
M is non empty V46() Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
M is non empty V46() (X,S)
meet M is Element of bool X
union M is Element of bool X
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
M is non empty V46() (X,S)
meet M is set
union M is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
F is non empty set
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is Element of F
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (m + 1) is Element of S
M . m is Element of S
(M . (m + 1)) \ (M . m) is Element of S
m9 is Element of F
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l is Element of F
k is Element of F
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (l + 1) is Element of S
M . l is Element of S
(M . (l + 1)) \ (M . l) is Element of S
[:NAT,F:] is non empty set
bool [:NAT,F:] is non empty set
G is Element of F
m is V1() V4( NAT ) V5(F) Function-like non empty V14( NAT ) V29( NAT ,F) Element of bool [:NAT,F:]
m . 0 is Element of F
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . (m + 1) is Element of F
M . (m + 1) is Element of S
M . m is Element of S
(M . (m + 1)) \ (M . m) is Element of S
m . m is Element of F
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m9 is Element of F
l is Element of F
k + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (k + 1) is Element of S
M . k is Element of S
(M . (k + 1)) \ (M . k) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
F is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G is Element of S
F + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (F + 1) is Element of S
(M . (F + 1)) \/ G is Element of S
m is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is Element of S
m9 is Element of S
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (l + 1) is Element of S
(M . (l + 1)) \/ m is Element of S
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (G + 1) is Element of S
M . (G + 1) is Element of S
F . G is Element of S
(M . (G + 1)) \/ (F . G) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is set
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . m is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . m is Element of S
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (m + 1) is Element of S
M . (m + 1) is Element of S
(M . (m + 1)) \/ (F . m) is set
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . m9 is Element of S
m is V15() V16() V17() V21() ext-real set
F . m is Element of S
m is V15() V16() V17() V21() ext-real set
F . m is Element of S
m9 is V15() V16() V17() V21() ext-real set
m9 + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . l is Element of S
M . m is Element of S
(M . m) \/ (F . l) is set
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . m9 is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . l is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . m is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . m is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (G + 1) is Element of S
(G + 1) + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . ((G + 1) + 1) is Element of S
M . ((G + 1) + 1) is Element of S
(M . ((G + 1) + 1)) \/ (F . (G + 1)) is set
0 + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (0 + 1) is Element of S
M . (0 + 1) is Element of S
(M . (0 + 1)) \/ (F . 0) is set
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . G is Element of S
m is V15() V16() V17() V21() ext-real set
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . G is Element of S
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (G + 1) is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . m is Element of S
m is set
M . (G + 1) is Element of S
(M . (G + 1)) \/ (F . G) is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
G . 0 is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . m is Element of S
F . m is Element of S
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . m9 is Element of S
F . m9 is Element of S
m9 + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . (m9 + 1) is Element of S
F . (m9 + 1) is Element of S
M . (m9 + 1) is Element of S
(M . (m9 + 1)) \/ (F . m9) is set
(M . (m9 + 1)) \ (F . m9) is Element of bool (M . (m9 + 1))
bool (M . (m9 + 1)) is non empty set
F . m is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is Element of S
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (G + 1) is Element of S
F . G is Element of S
(M . (G + 1)) \ (F . G) is Element of S
m is set
m9 is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l is Element of S
k is Element of S
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (l + 1) is Element of S
F . l is Element of S
(M . (l + 1)) \ (F . l) is Element of S
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
G . 0 is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . (m + 1) is Element of S
M . (m + 1) is Element of S
F . m is Element of S
(M . (m + 1)) \ (F . m) is Element of S
G . m is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is Element of S
m9 is Element of S
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (l + 1) is Element of S
F . l is Element of S
(M . (l + 1)) \ (F . l) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is Element of S
M . G is Element of S
(M . 0) \ (M . G) is Element of S
m is Element of S
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m9 is Element of S
l is Element of S
M . k is Element of S
(M . 0) \ (M . k) is Element of S
F is Element of S
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
G . 0 is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . (m + 1) is Element of S
M . m is Element of S
(M . 0) \ (M . m) is Element of S
G . m is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is Element of S
m9 is Element of S
M . l is Element of S
(M . 0) \ (M . l) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
G . 0 is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . m is Element of S
G . m is Element of S
m9 is V15() V16() V17() V21() ext-real set
m9 + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . (l + 1) is Element of S
M . (l + 1) is Element of S
F . l is Element of S
(M . (l + 1)) \ (F . l) is Element of S
(G . m) /\ (G . m) is Element of S
(G . m) /\ (F . l) is Element of S
((G . m) /\ (F . l)) /\ (G . (l + 1)) is Element of S
(F . l) /\ (G . (l + 1)) is Element of S
(G . m) /\ ((F . l) /\ (G . (l + 1))) is Element of S
(G . m) /\ {} is V58() V59() V60() V61() V62() V63() set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty set
bool [:S,ExtREAL:] is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V29(S, ExtREAL ) V74() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
F is non empty V46() (X,S)
(X,S,F) is Element of S
M . (X,S,F) is ext-real Element of ExtREAL
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
rng G is non empty Element of bool (bool X)
M * G is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
SUM (M * G) is ext-real Element of ExtREAL
Ser (M * G) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
rng (Ser (M * G)) is non empty V46() V59() Element of bool ExtREAL
sup (rng (Ser (M * G))) is ext-real Element of ExtREAL
G . 0 is Element of S
m is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
m . 0 is Element of S
m is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
m . 0 is Element of S
m9 is set
l is set
m . m9 is set
m . l is set
dom m is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
dom m is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
dom m is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
M * m is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
SUM (M * m) is ext-real Element of ExtREAL
Ser (M * m) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
rng (Ser (M * m)) is non empty V46() V59() Element of bool ExtREAL
sup (rng (Ser (M * m))) is ext-real Element of ExtREAL
rng m is non empty Element of bool (bool X)
union (rng m) is Element of bool X
M . (union (rng m)) is set
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . m9 is Element of S
G . m9 is Element of S
l is V15() V16() V17() V21() ext-real set
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . k is Element of S
(G . m9) \ (m . k) is Element of S
l is V15() V16() V17() V21() ext-real set
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
(M * m) . m9 is ext-real Element of ExtREAL
(M * G) . m9 is ext-real Element of ExtREAL
dom (M * G) is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
G . m9 is Element of S
M . (G . m9) is ext-real Element of ExtREAL
dom (M * m) is V58() V59() V60() V61() V62() V63() Element of bool NAT
m . m9 is Element of S
M . (m . m9) is ext-real Element of ExtREAL
union (rng G) is Element of bool X
m9 is set
l is set
dom m is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
k is set
m . k is set
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . l is Element of S
m9 is set
l is set
dom G is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
k is set
G . k is set
k is V15() V16() V17() V21() ext-real set
G . k is Element of S
k is V15() V16() V17() V21() ext-real set
G . k is Element of S
l is V15() V16() V17() V21() ext-real set
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . k is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . l is Element of S
i is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G . i is Element of S
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . (l + 1) is Element of S
G . (l + 1) is Element of S
(G . (l + 1)) \ (m . l) is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . l is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . l is Element of S
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . k is Element of S
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m . k is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is non empty V46() (X,S)
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
F is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V29( NAT , bool X) Element of bool [:NAT,(bool X):]
rng F is Element of bool (bool X)
bool (bool X) is non empty set
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
rng G is non empty Element of bool (bool X)
S is V1() Function-like set
S . 0 is set
X is V1() Function-like set
X . 0 is set
M is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . M is set
M + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . (M + 1) is set
(M + 1) + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . ((M + 1) + 1) is set
X . (M + 1) is set
(X . 0) \ (X . (M + 1)) is Element of bool (X . 0)
bool (X . 0) is non empty set
X . M is set
(X . 0) \ (X . M) is Element of bool (X . 0)
M is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . M is set
M + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . (M + 1) is set
0 + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . (0 + 1) is set
(X . 0) \ (X . 0) is Element of bool (X . 0)
bool (X . 0) is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V29(S, ExtREAL ) V74() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
F is non empty V46() (X,S)
(X,S,F) is Element of S
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
rng G is non empty Element of bool (bool X)
M * G is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
(M * G) . m is ext-real Element of ExtREAL
G . m is Element of S
M . (G . m) is ext-real Element of ExtREAL
SUM (M * G) is ext-real Element of ExtREAL
Ser (M * G) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
rng (Ser (M * G)) is non empty V46() V59() Element of bool ExtREAL
sup (rng (Ser (M * G))) is ext-real Element of ExtREAL
(Ser (M * G)) . 0 is ext-real Element of ExtREAL
(M * G) . 0 is ext-real Element of ExtREAL
M . (X,S,F) is ext-real Element of ExtREAL
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty set
bool [:S,ExtREAL:] is non empty set
G is set
F is non empty V46() (X,S)
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V29(S, ExtREAL ) V74() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
(X,S,F) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V29(S, ExtREAL ) V74() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
F is non empty V46() (X,S)
(X,S,F) is Element of S
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
G is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V29( NAT , bool X) Element of bool [:NAT,(bool X):]
rng G is Element of bool (bool X)
bool (bool X) is non empty set
G . 0 is Element of bool X
G is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
M is set
F is Element of bool X
G is Element of bool X
m is Element of bool X
{F} is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
{G,m} is non empty set
m is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V29( NAT , bool X) Element of bool [:NAT,(bool X):]
rng m is Element of bool (bool X)
bool (bool X) is non empty set
m . 0 is Element of bool X
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
m9 is non empty V46() (X,S)
l is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
rng l is non empty Element of bool (bool X)
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l . k is Element of S
k + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l . (k + 1) is Element of S
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l . k is Element of S
k + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l . (k + 1) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
M is set
F is Element of bool X
{F} is non empty set
bool X is non empty Element of bool (bool X)
[:NAT,(bool X):] is non empty set
bool [:NAT,(bool X):] is non empty set
{F,F} is non empty set
m is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V29( NAT , bool X) Element of bool [:NAT,(bool X):]
rng m is Element of bool (bool X)
bool (bool X) is non empty set
m . 0 is Element of bool X
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
m9 is non empty V46() (X,S)
l is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
rng l is non empty Element of bool (bool X)
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
k + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l . (k + 1) is Element of S
l . k is Element of S
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
k + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l . (k + 1) is Element of S
l . k is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
rng F is non empty Element of bool (bool X)
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . G is Element of S
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (G + 1) is Element of S
X is V1() Function-like set
S is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
X . S is set
S + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
X . (S + 1) is set
M is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
X . M is set
X . 0 is set
S is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
X . S is set
S is V1() Function-like set
S . 0 is set
X is V1() Function-like set
X . 0 is set
F is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . M is set
S . F is set
G is V15() V16() V17() V21() ext-real set
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . m is set
X . m is set
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . (m + 1) is set
X . (m + 1) is set
(X . (m + 1)) \ (X . m) is Element of bool (X . (m + 1))
bool (X . (m + 1)) is non empty set
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . m is set
X . m is set
X . m is set
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
S . (m + 1) is set
X . (m + 1) is set
X . m is set
(X . (m + 1)) \ (X . m) is Element of bool (X . (m + 1))
bool (X . (m + 1)) is non empty set
(S . M) /\ (S . (m + 1)) is set
(S . M) /\ (X . m) is set
((S . M) /\ (X . m)) /\ (S . (m + 1)) is set
(X . m) /\ (S . (m + 1)) is set
(S . M) /\ ((X . m) /\ (S . (m + 1))) is set
(S . M) /\ {} is V58() V59() V60() V61() V62() V63() set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
rng F is non empty Element of bool (bool X)
union (rng F) is Element of bool X
rng M is non empty Element of bool (bool X)
union (rng M) is Element of bool X
G is set
m is set
dom F is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
m is set
F . m is set
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l is V15() V16() V17() V21() ext-real set
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
k is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
k + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (k + 1) is Element of S
M . k is Element of S
(M . (k + 1)) \ (M . k) is Element of S
l is set
k is set
G is set
m is set
dom M is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
m is set
M . m is set
m is V15() V16() V17() V21() ext-real set
M . m is Element of S
m is V15() V16() V17() V21() ext-real set
M . m is Element of S
m9 is V15() V16() V17() V21() ext-real set
m9 + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . m is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . l is Element of S
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
l + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . (l + 1) is Element of S
M . (l + 1) is Element of S
(M . (l + 1)) \ (M . l) is Element of S
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . m9 is Element of S
l is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . l is Element of S
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
F . m is Element of S
m is set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is set
m is set
F . G is set
F . m is set
dom F is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
m9 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
dom F is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
dom F is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
F . 0 is Element of S
M is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
M . 0 is Element of S
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (G + 1) is Element of S
F . (G + 1) is Element of S
M . G is Element of S
(F . (G + 1)) \/ (M . G) is Element of S
(M . (G + 1)) \ (M . G) is Element of S
G is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
G + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
M . (G + 1) is Element of S
F . (G + 1) is Element of S
M . G is Element of S
(F . (G + 1)) \/ (M . G) is Element of S
X is set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V54() V55() V56() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty set
bool [:S,ExtREAL:] is non empty set
[:NAT,S:] is non empty set
bool [:NAT,S:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V29(S, ExtREAL ) V74() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
F is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
rng F is non empty Element of bool (bool X)
union (rng F) is Element of bool X
M . (union (rng F)) is set
M * F is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
rng (M * F) is non empty V46() V59() Element of bool ExtREAL
sup (rng (M * F)) is ext-real Element of ExtREAL
F . 0 is Element of S
G is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V29( NAT ,S) Element of bool [:NAT,S:]
G . 0 is Element of S
M * G is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
Ser (M * G) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V29( NAT , ExtREAL ) Element of bool [:NAT,ExtREAL:]
m is set
(Ser (M * G)) . m is set
(M * F) . m is set
m is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
(Ser (M * G)) . m is ext-real Element of ExtREAL
(M * F) . m is ext-real Element of ExtREAL
m + 1 is V15() V16() V17() V21() V22() ext-real V58() V59() V60() V61() V62() V63() V92() Element of NAT
(Ser (M * G)) . (m + 1) is ext-real Element of ExtREAL
(M * F) . (m + 1) is ext-real Element of ExtREAL
(M * G) . (m + 1) is ext-real Element of ExtREAL
G . (m + 1) is Element of S
M . (G . (m + 1)) is ext-real Element of ExtREAL
F . (m + 1) is Element of S
M . (F . (m + 1)) is ext-real Element of ExtREAL
F . m is Element of S
(F . (m + 1)) \ (F . m) is Element of S
((M * F) . m) + ((M * G) . (m + 1)) is ext-real Element of ExtREAL
M . (F . m) is ext-real Element of ExtREAL
(M . (F . m)) + (M . (G . (m + 1))) is ext-real Element of ExtREAL
(F . m) \/ (G . (m + 1)) is Element of S
M . ((F . m) \/ (G . (m + 1))) is ext-real Element of ExtREAL
(Ser (M * G)) . 0 is ext-real Element of ExtREAL
(M * G) . 0 is ext-real Element of ExtREAL
M . (F . 0) is ext-real Element of ExtREAL
(M * F) . 0 is ext-real Element of ExtREAL
dom (Ser (M * G)) is V58() V59() V60() V61() V62() V63() Element of bool NAT
bool NAT is non empty set
dom (M * F) is V58() V59() V60() V61() V62() V63() Element of bool NAT
rng G is non empty Element of bool (bool X)
union (rng G) is Element of bool X
M . (union (rng G)) is set
SUM (M * G) is ext-real Element of ExtREAL
rng (Ser (M * G)) is non empty V46() V59() Element of bool ExtREAL
sup (rng (Ser (M * G))) is ext-real Element of ExtREAL