:: MEASURE3 semantic presentation

REAL is non empty V33() V59() V60() V61() V65() set

NAT is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() Element of bool REAL

bool REAL is non empty set

ExtREAL is non empty V60() set

[:NAT,ExtREAL:] is non empty V67() set

bool [:NAT,ExtREAL:] is non empty set

bool ExtREAL is non empty set

omega is non empty epsilon-transitive epsilon-connected ordinal V59() V60() V61() V62() V63() V64() V65() set

bool omega is non empty set

[:NAT,REAL:] is non empty V66() V67() V68() set

bool [:NAT,REAL:] is non empty set

bool (bool REAL) is non empty set

RAT is non empty V33() V59() V60() V61() V62() V65() set

INT is non empty V33() V59() V60() V61() V62() V63() V65() set

{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() V65() set

the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() V65() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() V65() set

0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() V65() Element of NAT

1 is non empty epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL

+infty is V23() ext-real Element of ExtREAL

+infty is V23() set

-infty is V23() set

X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

Ser X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

Ser S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

SUM X is ext-real Element of ExtREAL

SUM S is ext-real Element of ExtREAL

rng (Ser X) is non empty V47() V60() Element of bool ExtREAL

rng (Ser S) is non empty V47() V60() Element of bool ExtREAL

M is ext-real set

dom (Ser X) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

A is set

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

B is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser S) . B is ext-real Element of ExtREAL

B2 is ext-real Element of ExtREAL

dom (Ser S) is V59() V60() V61() V62() V63() V64() Element of bool NAT

sup (rng (Ser X)) is ext-real Element of ExtREAL

sup (rng (Ser S)) is ext-real Element of ExtREAL

X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

Ser X is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

Ser S is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

SUM X is ext-real Element of ExtREAL

SUM S is ext-real Element of ExtREAL

M is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser S) . M is ext-real Element of ExtREAL

(Ser X) . M is ext-real Element of ExtREAL

M is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser X) . M is ext-real Element of ExtREAL

(Ser S) . M is ext-real Element of ExtREAL

X is set

bool X is non empty set

bool (bool X) 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 V55() V56() V57() 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 ) V30( NAT ,S) Element of bool [:NAT,S:]

rng M is set

rng M is non empty 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

(X,S,A) is non empty V47() N_Measure_fam of S

meet (X,S,A) is Element of S

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

B is Element of S

M . B is ext-real Element of ExtREAL

B2 is set

C2 is set

dom A is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C1 is set

A . C1 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 V55() V56() V57() 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 ) V30( NAT ,S) Element of bool [:NAT,S:]

M . 0 is Element of S

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

(X,S,M) is non empty V47() N_Measure_fam of S

union (X,S,M) is Element of S

(X,S,A) is non empty V47() N_Measure_fam of S

meet (X,S,A) is Element of S

(A . 0) \ (meet (X,S,A)) is Element of S

dom M is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

B is set

B2 is set

C2 is set

M . C2 is set

C1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real set

D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . O is Element of S

(A . 0) \ (A . O) is Element of S

B is set

B2 is set

B2 is set

dom A is V59() V60() V61() V62() V63() V64() Element of bool NAT

C2 is set

A . C2 is set

C1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . C1 is Element of S

(A . 0) \ (A . C1) is Element of S

C1 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

M . (C1 + 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 V55() V56() V57() 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 ) V30( NAT ,S) Element of bool [:NAT,S:]

M . 0 is Element of S

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

(X,S,A) is non empty V47() N_Measure_fam of S

meet (X,S,A) is Element of S

(X,S,M) is non empty V47() N_Measure_fam of S

union (X,S,M) is Element of S

(A . 0) \ (union (X,S,M)) is Element of S

B is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B is Element of S

B + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . (B + 1) is Element of S

the Element of (X,S,A) is Element of (X,S,A)

B2 is set

dom A is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C2 is set

A . C2 is set

(A . 0) /\ (meet (X,S,A)) is Element of S

(A . 0) \ (meet (X,S,A)) is Element of S

(A . 0) \ ((A . 0) \ (meet (X,S,A))) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

M . (B . 0) is ext-real Element of ExtREAL

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

(X,S,B) is non empty V47() N_Measure_fam of S

meet (X,S,B) is Element of S

M . (meet (X,S,B)) is ext-real Element of ExtREAL

(X,S,A) is non empty V47() N_Measure_fam of S

union (X,S,A) is Element of S

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

(M . (B . 0)) - (M . (union (X,S,A))) is ext-real Element of ExtREAL

K183((M . (union (X,S,A)))) is ext-real set

K182((M . (B . 0)),K183((M . (union (X,S,A))))) is ext-real set

(B . 0) \ (meet (X,S,B)) is Element of S

(B . 0) \ (union (X,S,A)) is Element of S

M . ((B . 0) \ (union (X,S,A))) is ext-real Element of ExtREAL

M . ((B . 0) \ (meet (X,S,B))) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

M . (B . 0) is ext-real Element of ExtREAL

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

(X,S,A) is non empty V47() N_Measure_fam of S

union (X,S,A) is Element of S

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

(X,S,B) is non empty V47() N_Measure_fam of S

meet (X,S,B) is Element of S

M . (meet (X,S,B)) is ext-real Element of ExtREAL

(M . (B . 0)) - (M . (meet (X,S,B))) is ext-real Element of ExtREAL

K183((M . (meet (X,S,B)))) is ext-real set

K182((M . (B . 0)),K183((M . (meet (X,S,B))))) is ext-real set

(B . 0) \ (union (X,S,A)) is Element of S

(B . 0) \ (meet (X,S,B)) is Element of S

M . ((B . 0) \ (meet (X,S,B))) is ext-real Element of ExtREAL

M . ((B . 0) \ (union (X,S,A))) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

M . (B . 0) is ext-real Element of ExtREAL

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

(X,S,B) is non empty V47() N_Measure_fam of S

meet (X,S,B) is Element of S

M . (meet (X,S,B)) is ext-real Element of ExtREAL

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * A) is non empty V47() V60() Element of bool ExtREAL

sup (rng (M * A)) is ext-real Element of ExtREAL

(M . (B . 0)) - (sup (rng (M * A))) is ext-real Element of ExtREAL

K183((sup (rng (M * A)))) is ext-real set

K182((M . (B . 0)),K183((sup (rng (M * A))))) is ext-real set

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B2 is Element of S

B2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . (B2 + 1) is Element of S

(X,S,A) is non empty V47() N_Measure_fam of S

union (X,S,A) is Element of S

M . (union (X,S,A)) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

M . (B . 0) is ext-real Element of ExtREAL

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * B) is non empty V47() V60() Element of bool ExtREAL

inf (rng (M * B)) is ext-real Element of ExtREAL

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * A) is non empty V47() V60() Element of bool ExtREAL

sup (rng (M * A)) is ext-real Element of ExtREAL

B2 is Element of S

M . B2 is ext-real Element of ExtREAL

C2 is ext-real set

dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C1 is set

(M * A) . C1 is ext-real Element of ExtREAL

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . D2 is Element of S

M . (A . D2) is ext-real Element of ExtREAL

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real set

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S

(B . 0) \ (B . B2) is Element of S

C2 is ext-real set

dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C1 is set

(M * B) . C1 is ext-real Element of ExtREAL

(M * B) . 0 is ext-real Element of ExtREAL

dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C2 is ext-real Element of ExtREAL

(M * A) . 0 is ext-real Element of ExtREAL

C1 is ext-real Element of ExtREAL

dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

D2 is set

(M * A) . D2 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

M . (B . 0) is ext-real Element of ExtREAL

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * A) is non empty V47() V60() Element of bool ExtREAL

sup (rng (M * A)) is ext-real Element of ExtREAL

M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * B) is non empty V47() V60() Element of bool ExtREAL

inf (rng (M * B)) is ext-real Element of ExtREAL

(M . (B . 0)) - (inf (rng (M * B))) is ext-real Element of ExtREAL

K183((inf (rng (M * B)))) is ext-real set

K182((M . (B . 0)),K183((inf (rng (M * B))))) is ext-real set

C2 is ext-real set

dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C1 is set

(M * A) . C1 is ext-real Element of ExtREAL

-infty is V23() ext-real Element of ExtREAL

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . D2 is Element of S

dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT

(B . 0) \ (A . D2) is Element of S

M . ((B . 0) \ (A . D2)) is ext-real Element of ExtREAL

(M * B) . 0 is ext-real Element of ExtREAL

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . O is Element of S

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . (O + 1) is Element of S

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real set

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S

M . (B . B2) is ext-real Element of ExtREAL

(M * B) . B2 is ext-real Element of ExtREAL

(B . 0) \ (B . B2) is Element of S

(B . 0) \ ((B . 0) \ (B . B2)) is Element of S

(B . 0) /\ (B . B2) is Element of S

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real set

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S

(B . 0) \ (B . B2) is Element of S

M . (A . D2) is ext-real Element of ExtREAL

O is ext-real Element of ExtREAL

B2 is V22() V23() ext-real Element of REAL

D2 is V22() V23() ext-real Element of REAL

O1 is V22() V23() ext-real Element of REAL

(M . (B . 0)) - O is ext-real Element of ExtREAL

K183(O) is ext-real set

K182((M . (B . 0)),K183(O)) is ext-real set

B2 - D2 is V22() V23() ext-real Element of REAL

((M . (B . 0)) - O) + O is ext-real Element of ExtREAL

(B2 - D2) + D2 is V22() V23() ext-real Element of REAL

(inf (rng (M * B))) + O is ext-real Element of ExtREAL

O1 + D2 is V22() V23() ext-real Element of REAL

((inf (rng (M * B))) + O) - (inf (rng (M * B))) is ext-real Element of ExtREAL

K182(((inf (rng (M * B))) + O),K183((inf (rng (M * B))))) is ext-real set

D2 + O1 is V22() V23() ext-real Element of REAL

(D2 + O1) - O1 is V22() V23() ext-real Element of REAL

C2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . C2 is Element of S

C2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . (C2 + 1) is Element of S

C2 is ext-real UpperBound of rng (M * A)

(X,S,B) is non empty V47() N_Measure_fam of S

meet (X,S,B) is Element of S

M . (meet (X,S,B)) is ext-real Element of ExtREAL

C1 is ext-real set

dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

D2 is set

(M * B) . D2 is ext-real Element of ExtREAL

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . O is Element of S

M . (B . O) is ext-real Element of ExtREAL

(X,S,A) is non empty V47() N_Measure_fam of S

union (X,S,A) is Element of S

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

(M . (B . 0)) - (M . (meet (X,S,B))) is ext-real Element of ExtREAL

K183((M . (meet (X,S,B)))) is ext-real set

K182((M . (B . 0)),K183((M . (meet (X,S,B))))) is ext-real 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

M . (B . 0) is ext-real Element of ExtREAL

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * B) is non empty V47() V60() Element of bool ExtREAL

inf (rng (M * B)) is ext-real Element of ExtREAL

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * A) is non empty V47() V60() Element of bool ExtREAL

sup (rng (M * A)) is ext-real Element of ExtREAL

(M . (B . 0)) - (sup (rng (M * A))) is ext-real Element of ExtREAL

K183((sup (rng (M * A)))) is ext-real set

K182((M . (B . 0)),K183((sup (rng (M * A))))) is ext-real set

C2 is ext-real set

dom (M * B) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

C1 is set

(M * B) . C1 is ext-real Element of ExtREAL

D2 is ext-real Element of ExtREAL

O is V22() V23() ext-real Element of REAL

B2 is V22() V23() ext-real Element of REAL

D2 is V22() V23() ext-real Element of REAL

(sup (rng (M * A))) + D2 is ext-real Element of ExtREAL

D2 + B2 is V22() V23() ext-real Element of REAL

((sup (rng (M * A))) + D2) - (sup (rng (M * A))) is ext-real Element of ExtREAL

K182(((sup (rng (M * A))) + D2),K183((sup (rng (M * A))))) is ext-real set

B2 + D2 is V22() V23() ext-real Element of REAL

(B2 + D2) - D2 is V22() V23() ext-real Element of REAL

dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT

(M . (B . 0)) - D2 is ext-real Element of ExtREAL

K183(D2) is ext-real set

K182((M . (B . 0)),K183(D2)) is ext-real set

O1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

O1 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

c

B . c

c

B . (c

B . O1 is Element of S

M . (B . O1) is ext-real Element of ExtREAL

(M . (B . 0)) - (M . (B . O1)) is ext-real Element of ExtREAL

K183((M . (B . O1))) is ext-real set

K182((M . (B . 0)),K183((M . (B . O1)))) is ext-real set

(B . 0) \ (B . O1) is Element of S

M . ((B . 0) \ (B . O1)) is ext-real Element of ExtREAL

A . (O1 + 1) is Element of S

M . (A . (O1 + 1)) is ext-real Element of ExtREAL

(M * A) . (O1 + 1) is ext-real Element of ExtREAL

O - B2 is V22() V23() ext-real Element of REAL

((M . (B . 0)) - D2) + D2 is ext-real Element of ExtREAL

(O - B2) + B2 is V22() V23() ext-real Element of REAL

C2 is V22() V23() ext-real Element of REAL

C1 is V22() V23() ext-real Element of REAL

D2 is V22() V23() ext-real Element of REAL

(sup (rng (M * A))) + (inf (rng (M * B))) is ext-real Element of ExtREAL

C2 + D2 is V22() V23() ext-real Element of REAL

((sup (rng (M * A))) + (inf (rng (M * B)))) - (sup (rng (M * A))) is ext-real Element of ExtREAL

K182(((sup (rng (M * A))) + (inf (rng (M * B)))),K183((sup (rng (M * A))))) is ext-real set

D2 + C2 is V22() V23() ext-real Element of REAL

(D2 + C2) - C2 is V22() V23() ext-real Element of REAL

O is ext-real LowerBound of rng (M * B)

(M . (B . 0)) - (inf (rng (M * B))) is ext-real Element of ExtREAL

K183((inf (rng (M * B)))) is ext-real set

K182((M . (B . 0)),K183((inf (rng (M * B))))) is ext-real set

B2 is ext-real Element of ExtREAL

D2 is ext-real Element of ExtREAL

O1 is ext-real Element of ExtREAL

C1 - D2 is V22() V23() ext-real Element of REAL

((M . (B . 0)) - (inf (rng (M * B)))) + O1 is ext-real Element of ExtREAL

(C1 - D2) + D2 is V22() V23() ext-real Element of REAL

X is set

bool X is non empty set

bool (bool X) is non empty set

S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

A . 0 is Element of S

M . (A . 0) is ext-real Element of ExtREAL

(X,S,A) is non empty V47() N_Measure_fam of S

meet (X,S,A) is Element of S

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

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * A) is non empty V47() V60() Element of bool ExtREAL

inf (rng (M * A)) is ext-real Element of ExtREAL

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B . 0 is Element of S

(X,S,B) is non empty V47() N_Measure_fam of S

union (X,S,B) is Element of S

(A . 0) \ (meet (X,S,A)) is Element of S

(A . 0) \ (union (X,S,B)) is Element of S

M . ((A . 0) \ (union (X,S,B))) is ext-real Element of ExtREAL

B2 is Element of S

M . B2 is ext-real Element of ExtREAL

(M . (A . 0)) - (M . B2) is ext-real Element of ExtREAL

K183((M . B2)) is ext-real set

K182((M . (A . 0)),K183((M . B2))) is ext-real set

M . ((A . 0) \ (meet (X,S,A))) is ext-real Element of ExtREAL

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S

B2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . (B2 + 1) is Element of S

M . (union (X,S,B)) is ext-real Element of ExtREAL

M * B is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

rng (M * B) is non empty V47() V60() Element of bool ExtREAL

sup (rng (M * B)) is ext-real Element of ExtREAL

(M . (A . 0)) - (sup (rng (M * B))) is ext-real Element of ExtREAL

K183((sup (rng (M * B)))) is ext-real set

K182((M . (A . 0)),K183((sup (rng (M * B))))) is ext-real 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative V90(X,S) Element of bool [:S,ExtREAL:]

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) V53() Element of bool [:NAT,S:]

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

SUM (M * A) is ext-real Element of ExtREAL

(X,S,A) is non empty V47() N_Measure_fam of S

union (X,S,A) is Element of S

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

A . 0 is Element of S

B2 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B2 . 0 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

{(union (X,S,A)),{}} is non empty set

C2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

rng C2 is Element of bool (bool X)

bool (bool X) is non empty set

C2 . 0 is Element of bool X

C1 is set

Ser (M * A) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

dom (M * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . D2 is Element of S

D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . (D2 + 1) is Element of S

(B2 . D2) /\ (A . (D2 + 1)) is Element of S

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . O is Element of S

O + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . (O + 1) is Element of S

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B2 is Element of S

(B2 . (O + 1)) /\ (A . B2) is Element of S

A . (O + 1) is Element of S

(A . (O + 1)) /\ (A . B2) is Element of S

(A . (O + 1)) \/ (B2 . O) is Element of S

((A . (O + 1)) \/ (B2 . O)) /\ (A . B2) is Element of S

(B2 . O) /\ (A . B2) is Element of S

((A . (O + 1)) /\ (A . B2)) \/ ((B2 . O) /\ (A . B2)) is Element of S

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . O is Element of S

(B2 . 0) /\ (A . O) is Element of S

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (M * A)) . D2 is ext-real Element of ExtREAL

B2 . D2 is Element of S

M . (B2 . D2) is ext-real Element of ExtREAL

D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (M * A)) . (D2 + 1) is ext-real Element of ExtREAL

B2 . (D2 + 1) is Element of S

M . (B2 . (D2 + 1)) is ext-real Element of ExtREAL

A . (D2 + 1) is Element of S

(B2 . D2) /\ (A . (D2 + 1)) is Element of S

(M * A) . (D2 + 1) is ext-real Element of ExtREAL

(M . (B2 . D2)) + ((M * A) . (D2 + 1)) is ext-real Element of ExtREAL

M . (A . (D2 + 1)) is ext-real Element of ExtREAL

(M . (B2 . D2)) + (M . (A . (D2 + 1))) is ext-real Element of ExtREAL

(A . (D2 + 1)) \/ (B2 . D2) is Element of S

M . ((A . (D2 + 1)) \/ (B2 . D2)) is ext-real Element of ExtREAL

(Ser (M * A)) . 0 is ext-real Element of ExtREAL

(M * A) . 0 is ext-real Element of ExtREAL

M . (B2 . 0) is ext-real Element of ExtREAL

C1 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

M * C1 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

Ser (M * C1) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (M * C1)) . D2 is ext-real Element of ExtREAL

D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (M * C1)) . (D2 + 1) is ext-real Element of ExtREAL

C1 . (D2 + 1) is Element of S

dom (M * C1) is V59() V60() V61() V62() V63() V64() Element of bool NAT

(M * C1) . (D2 + 1) is ext-real Element of ExtREAL

M . {} is ext-real Element of ExtREAL

(M . (union (X,S,A))) + ((M * C1) . (D2 + 1)) is ext-real Element of ExtREAL

(Ser (M * C1)) . 0 is ext-real Element of ExtREAL

(M * C1) . 0 is ext-real Element of ExtREAL

dom (M * C1) is V59() V60() V61() V62() V63() V64() Element of bool NAT

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(M * C1) . D2 is ext-real Element of ExtREAL

0 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

C1 . D2 is Element of S

M . {} is ext-real Element of ExtREAL

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . D2 is Element of S

D2 + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . (D2 + 1) is Element of S

A . (D2 + 1) is Element of S

(A . (D2 + 1)) \/ (B2 . D2) is Element of S

D2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (M * A)) . D2 is ext-real Element of ExtREAL

(Ser (M * C1)) . D2 is ext-real Element of ExtREAL

B2 . D2 is Element of S

M . (B2 . D2) is ext-real Element of ExtREAL

SUM (M * C1) is ext-real Element of ExtREAL

(Ser (M * C1)) . 1 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative V90(X,S) Element of bool [:S,ExtREAL:]

A is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) V53() Element of bool [:NAT,S:]

M * A is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

SUM (M * A) is ext-real Element of ExtREAL

(X,S,A) is non empty V47() N_Measure_fam of S

union (X,S,A) is Element of S

M . (union (X,S,A)) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is Element of bool X

B is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() V65() set

M . B 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is set

M . A is ext-real Element of ExtREAL

B is set

M . B is ext-real Element of ExtREAL

B is set

B2 is set

A is (X,S,M)

B2 \/ A is set

bool X is non empty Element of bool (bool X)

A is set

B is set

B2 is set

B2 is set

C2 is (X,S,M)

B2 \/ C2 is set

B2 is set

C2 is set

C1 is (X,S,M)

C2 \/ C1 is set

B2 is set

C2 is (X,S,M)

B2 \/ C2 is set

B is set

B is non empty Element of bool (bool X)

B2 is set

C1 is set

C2 is set

D2 is (X,S,M)

C1 \/ D2 is set

A is non empty Element of bool (bool X)

B is non empty Element of bool (bool X)

B2 is set

C2 is set

C1 is (X,S,M)

C2 \/ C1 is set

C2 is set

C1 is (X,S,M)

C2 \/ C1 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

(X,S,M) is non empty Element of bool (bool X)

A is Element of (X,S,M)

bool X is non empty Element of bool (bool X)

B is set

B2 is set

A \ B2 is Element of bool X

C2 is set

A \ C2 is Element of bool X

B2 is set

B2 is set

C2 is (X,S,M)

B2 \/ C2 is set

C2 is (X,S,M)

B2 \/ C2 is set

C1 is set

M . C1 is ext-real Element of ExtREAL

A \ B2 is Element of bool X

C2 \ B2 is Element of bool X

B2 is non empty Element of bool (bool X)

C2 is set

A \ C2 is Element of bool X

C1 is set

A \ C1 is Element of bool X

B is non empty Element of bool (bool X)

B2 is non empty Element of bool (bool X)

C2 is set

A \ C2 is Element of bool X

A \ C2 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

(X,S,M) is non empty Element of bool (bool X)

[:NAT,(X,S,M):] is non empty set

bool [:NAT,(X,S,M):] is non empty set

A is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) Element of bool [:NAT,(X,S,M):]

B is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B is Element of (X,S,M)

(X,S,M,(A . B)) is non empty Element of bool (bool X)

the Element of (X,S,M,(A . B)) is Element of (X,S,M,(A . B))

C2 is Element of S

C1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

D2 is set

A . C1 is Element of (X,S,M)

(X,S,M,(A . C1)) is non empty Element of bool (bool X)

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . B2 is Element of S

A . B2 is Element of (X,S,M)

(X,S,M,(A . B2)) is non empty Element of bool (bool X)

X is set

bool X is non empty set

bool (bool X) 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

S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

(X,S,M) is non empty Element of bool (bool X)

[:NAT,(X,S,M):] is non empty set

bool [:NAT,(X,S,M):] is non empty set

A is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) Element of bool [:NAT,(X,S,M):]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B2 is Element of (X,S,M)

B . B2 is Element of S

(A . B2) \ (B . B2) is Element of bool (A . B2)

bool (A . B2) is non empty set

C2 is Element of bool X

C1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

D2 is set

A . C1 is Element of (X,S,M)

B . C1 is Element of S

(A . C1) \ (B . C1) is Element of bool (A . C1)

bool (A . C1) is non empty set

B2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

B2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

C2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . C2 is Element of bool X

A . C2 is Element of (X,S,M)

B . C2 is Element of S

(A . C2) \ (B . C2) is Element of bool (A . C2)

bool (A . C2) is non empty set

X is set

bool X is non empty set

bool (bool X) 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

S is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() 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) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

B is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B is Element of bool X

B2 is set

M . B2 is ext-real Element of ExtREAL

C2 is Element of S

C1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

D2 is set

A . C1 is Element of bool X

M . D2 is ext-real Element of ExtREAL

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

A . B2 is Element of bool X

B . B2 is Element of S

C2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B . C2 is Element of S

M . (B . C2) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is non empty Element of bool (bool X)

B is non empty V47() Element of bool (bool X)

union B is Element of bool X

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

B2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

rng B2 is Element of bool (bool X)

bool (bool X) is non empty set

C2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . C2 is Element of bool X

C2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . C2 is Element of bool X

(X,S,M) is non empty Element of bool (bool X)

C2 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

B2 . C2 is Element of bool X

C1 is set

D2 is (X,S,M)

C1 \/ D2 is set

C2 is set

B2 . C2 is set

dom B2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

[:NAT,(X,S,M):] is non empty set

bool [:NAT,(X,S,M):] is non empty set

[:NAT,S:] is non empty set

bool [:NAT,S:] is non empty set

C2 is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) Element of bool [:NAT,(X,S,M):]

C1 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

D2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

C1 . O is Element of S

C2 . O is Element of (X,S,M)

(C2 . O) \ (C1 . O) is Element of bool (C2 . O)

bool (C2 . O) is non empty set

(X,S,M,(C2 . O)) is non empty Element of bool (bool X)

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

D2 . O is Element of bool X

C2 . O is Element of (X,S,M)

C1 . O is Element of S

(C2 . O) \ (C1 . O) is Element of bool (C2 . O)

bool (C2 . O) is non empty set

O is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

(X,S,C1) is non empty V47() N_Measure_fam of S

union (X,S,C1) is Element of S

rng C2 is Element of bool (X,S,M)

bool (X,S,M) is non empty set

union (rng C2) is set

D2 is set

O1 is set

dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT

c

C1 . c

c

C2 . c

C1 . c

n is set

(X,S,O) is non empty V47() N_Measure_fam of S

D2 is set

dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT

O1 is Element of S

M . O1 is ext-real Element of ExtREAL

c

O . c

union (X,S,O) is Element of S

M . (union (X,S,O)) is ext-real Element of ExtREAL

(union B) \ (union (X,S,C1)) is Element of bool X

(union (rng C2)) /\ (union (X,S,C1)) is Element of bool X

((union B) \ (union (X,S,C1))) \/ ((union (rng C2)) /\ (union (X,S,C1))) is Element of bool X

(union (X,S,C1)) \/ ((union B) \ (union (X,S,C1))) is Element of bool X

O1 is Element of bool X

rng D2 is Element of bool (bool X)

union (rng D2) is Element of bool X

c

c

n is set

C2 . n is set

n is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

C1 . n is Element of S

dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT

C2 . n is Element of (X,S,M)

(C2 . n) \ (C1 . n) is Element of bool (C2 . n)

bool (C2 . n) is non empty set

D2 . n is Element of bool X

dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

c

c

c

dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

n is set

D2 . n is set

n is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT

O . n is Element of S

D2 . n is Element of bool X

c

(union (X,S,C1)) \/ c

D2 is (X,S,M)

(union (X,S,C1)) \/ D2 is Element of bool X

B2 is set

D2 is (X,S,M)

B2 \/ D2 is set

B is set

X \ B is Element of bool X

B2 is set

X \ B2 is Element of bool X

C1 is (X,S,M)

B2 \/ C1 is set

C1 is (X,S,M)

B2 \/ C1 is set

D2 is set

M . D2 is ext-real Element of ExtREAL

(X \ B2) \ D2 is Element of bool X

(X \ B2) \ C1 is Element of bool X

D2 \ C1 is Element of bool D2

bool D2 is non empty set

(X \ B2) /\ (D2 \ C1) is Element of bool D2

D2 is Element of bool X

O1 is (X,S,M)

((X \ B2) \ D2) \/ O1 is Element of bool X

B2 is (X,S,M)

((X \ B2) \ D2) \/ B2 is Element of bool X

B2 is set

C2 is (X,S,M)

B2 \/ C2 is set

B is non empty compl-closed sigma-multiplicative V55() V56() V57() 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

(X,S,M) is non empty Element of bool (bool X)

A is set

B2 is set

B is set

C2 is (X,S,M)

B2 \/ C2 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

A is set

B is set

M . A is ext-real Element of ExtREAL

M . B is ext-real Element of ExtREAL

B2 is (X,S,M)

A \/ B2 is set

C2 is (X,S,M)

B \/ C2 is set

C1 is set

M . C1 is ext-real Element of ExtREAL

A \/ C1 is set

D2 is set

M . D2 is ext-real Element of ExtREAL

B \/ D2 is set

O is Element of S

D2 is Element of S

O \/ D2 is Element of S

M . (O \/ D2) is ext-real Element of ExtREAL

M . O is ext-real Element of ExtREAL

M . D2 is ext-real Element of ExtREAL

(M . O) + (M . D2) is ext-real Element of ExtREAL

B2 is Element of S

M . B2 is ext-real Element of ExtREAL

O1 is Element of S

B2 \/ O1 is Element of S

M . (B2 \/ O1) is ext-real Element of ExtREAL

M . O1 is ext-real Element of ExtREAL

(M . B2) + (M . O1) 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 V55() V56() V57() sigma-additive Element of bool (bool X)

[:S,ExtREAL:] is non empty V67() set

bool [:S,ExtREAL:] is non empty set

M is V1() V4(S) V5( ExtREAL ) Function-like non empty V14(S) V30(S, ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:S,ExtREAL:]

(X,S,M) is non empty compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)

[:(X,S,M),ExtREAL:] is non empty V67() set

bool [:(X,S,M),ExtREAL:] is non empty set

M . {} is ext-real Element of ExtREAL

B2 is set

M . B2 is ext-real Element of ExtREAL

B2 is set

C2 is set

M . C2 is ext-real Element of ExtREAL

C1 is set

D2 is set

O is set

B2 is (X,S,M)

O \/ B2 is set

M . O is ext-real Element of ExtREAL

D2 is (X,S,M)

C2 \/ D2 is set

B2 is V1() V4((X,S,M)) V5( ExtREAL ) Function-like non empty V14((X,S,M)) V30((X,S,M), ExtREAL ) V67() Element of bool [:(X,S,M),ExtREAL:]

C2 is set

M . C2 is ext-real Element of ExtREAL

C1 is (X,S,M)

C2 \/ C1 is set

B2 . (C2 \/ C1) is ext-real Element of ExtREAL

[:NAT,(X,S,M):] is non empty set

bool [:NAT,(X,S,M):] is non empty set

C2 is V1() V4( NAT ) V5((X,S,M)) Function-like non empty V14( NAT ) V30( NAT ,(X,S,M)) V53() Element of bool [:NAT,(X,S,M):]

B2 * C2 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]

SUM (B2 * C2) is ext-real Element of ExtREAL

(X,(X,S,M),C2) is non empty V47() N_Measure_fam of (X,S,M)

union (X,(X,S,M),C2) is Element of (X,S,M)

B2 . (union (X,(X,S,M),C2)) is ext-real Element of ExtREAL

[:NAT,S:] is non empty set

bool [:NAT,S:] is non empty set

C1 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,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

D2 is V1() V4( NAT ) V5( bool X) Function-like non empty V14( NAT ) V30( NAT , bool X) Element of bool [:NAT,(bool X):]

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

C1 . O is Element of S

C2 . O is Element of (X,S,M)

(C2 . O) \ (C1 . O) is Element of bool (C2 . O)

bool (C2 . O) is non empty set

(X,S,M,(C2 . O)) is non empty Element of bool (bool X)

O is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

D2 . O is Element of bool X

C2 . O is Element of (X,S,M)

C1 . O is Element of S

(C2 . O) \ (C1 . O) is Element of bool (C2 . O)

bool (C2 . O) is non empty set

O is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) Element of bool [:NAT,S:]

B2 is set

D2 is set

C1 . B2 is set

C1 . D2 is set

dom C2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT

O1 is set

C1 . O1 is set

C2 . O1 is set

C2 . B2 is set

C2 . D2 is set

(C2 . B2) /\ (C2 . D2) is set

(C1 . B2) /\ (C1 . D2) is set

(X,S,C1) is non empty V47() N_Measure_fam of S

union (X,S,C1) is Element of S

B2 is set

dom C2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

D2 is set

O1 is set

dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT

c

C1 . c

c

C2 . c

C1 . c

n is set

(X,S,O) is non empty V47() N_Measure_fam of S

D2 is set

dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT

O1 is Element of S

M . O1 is ext-real Element of ExtREAL

c

O . c

union (X,S,O) is Element of S

M . (union (X,S,O)) is ext-real Element of ExtREAL

(union (X,(X,S,M),C2)) \ B2 is Element of bool X

(union (X,(X,S,M),C2)) /\ B2 is Element of bool X

((union (X,(X,S,M),C2)) \ B2) \/ ((union (X,(X,S,M),C2)) /\ B2) is Element of bool X

B2 \/ ((union (X,(X,S,M),C2)) \ B2) is set

O1 is Element of bool X

rng D2 is Element of bool (bool X)

bool (bool X) is non empty set

union (rng D2) is Element of bool X

c

c

n is set

C2 . n is set

n is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

C1 . n is Element of S

dom C1 is V59() V60() V61() V62() V63() V64() Element of bool NAT

C2 . n is Element of (X,S,M)

(C2 . n) \ (C1 . n) is Element of bool (C2 . n)

bool (C2 . n) is non empty set

D2 . n is Element of bool X

dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

c

c

c

dom D2 is V59() V60() V61() V62() V63() V64() Element of bool NAT

n is set

D2 . n is set

n is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

dom O is V59() V60() V61() V62() V63() V64() Element of bool NAT

O . n is Element of S

D2 . n is Element of bool X

c

B2 \/ c

D2 is V1() V4( NAT ) V5(S) Function-like non empty V14( NAT ) V30( NAT ,S) V53() Element of bool [:NAT,S:]

O1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT

C2 . O1 is Element of (X,S,M)

B2 . (C2 . O1) is ext-real Element of ExtREAL

D2 . O1 is Element of S

M . (D2 . O1) is ext-real Element of ExtREAL

(C2 . O1) \ (D2 . O1) is Element of bool (C2 . O1)

bool (C2 . O1) is non empty set

c

(C2 . O1) /\ (D2 . O1) is set