:: MEASURE2 semantic presentation

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