:: 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₁₅ is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B . c₁₅ is Element of S
c₁₅ + 1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
B . (c₁₅ + 1) is Element of S
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₁₄ is set
C1 . c₁₄ is set
c₁₅ is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
C2 . c₁₅ is Element of (X,S,M)
C1 . c₁₅ is Element of S
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₁₄ is set
O . c₁₄ is set
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₁₄ is set
c₁₅ is set
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₁₈ is set
c₁₄ is set
c₁₅ is set
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₁₄ is (X,S,M)
(union (X,S,C1)) \/ c₁₄ is Element of bool X
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₁₄ is set
C1 . c₁₄ is set
c₁₅ is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
C2 . c₁₅ is Element of (X,S,M)
C1 . c₁₅ is Element of S
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₁₄ is set
O . c₁₄ is set
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₁₄ is set
c₁₅ is set
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₁₈ is set
c₁₄ is set
c₁₅ is set
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₁₄ is (X,S,M)
B2 \/ c₁₄ is set
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₁₄ is (X,S,M)
(C2 . O1) /\ (D2 . O1) is set
((C2 . O1) /\ (D2 . O1)) \/ ((C2 . O1) \ (D2 . O1)) is set
(D2 . O1) \/ c₁₄ is set
M * D2 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) V67() Element of bool [:NAT,ExtREAL:]
O1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
(B2 * C2) . O1 is ext-real Element of ExtREAL
(M * D2) . O1 is ext-real Element of ExtREAL
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
O1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
(M * D2) . O1 is ext-real Element of ExtREAL
(B2 * C2) . O1 is ext-real Element of ExtREAL
SUM (M * D2) is ext-real Element of ExtREAL
O1 is epsilon-transitive epsilon-connected ordinal natural V22() V23() ext-real V59() V60() V61() V62() V63() V64() Element of NAT
(B2 * C2) . O1 is ext-real Element of ExtREAL
(M * D2) . O1 is ext-real Element of ExtREAL
(X,S,D2) is non empty V47() N_Measure_fam of S
union (X,S,D2) is Element of S
M . (union (X,S,D2)) is ext-real Element of ExtREAL
O1 is (X,S,M)
B2 \/ O1 is set
C2 is Element of (X,S,M)
B2 . C2 is ext-real Element of ExtREAL
C1 is set
D2 is Element of S
M . D2 is ext-real Element of ExtREAL
O is (X,S,M)
C1 \/ O is set
B is (X,S,M)
{} \/ B is set
B2 . {} is ext-real Element of ExtREAL
M . {} is ext-real Element of ExtREAL
C2 is V1() V4((X,S,M)) V5( ExtREAL ) Function-like non empty V14((X,S,M)) V30((X,S,M), ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:(X,S,M),ExtREAL:]
C1 is set
D2 is (X,S,M)
C1 \/ D2 is set
C2 . (C1 \/ D2) is ext-real Element of ExtREAL
M . C1 is ext-real Element of ExtREAL
A is V1() V4((X,S,M)) V5( ExtREAL ) Function-like non empty V14((X,S,M)) V30((X,S,M), ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:(X,S,M),ExtREAL:]
B is V1() V4((X,S,M)) V5( ExtREAL ) Function-like non empty V14((X,S,M)) V30((X,S,M), ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:(X,S,M),ExtREAL:]
B2 is set
A . B2 is ext-real Element of ExtREAL
B . B2 is ext-real Element of ExtREAL
C2 is set
M . C2 is ext-real Element of ExtREAL
C1 is (X,S,M)
C2 \/ C1 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 compl-closed sigma-multiplicative V55() V56() V57() sigma-additive Element of bool (bool X)
(X,S,M) is V1() V4((X,S,M)) V5( ExtREAL ) Function-like non empty V14((X,S,M)) V30((X,S,M), ExtREAL ) V67() V75() nonnegative sigma-additive Element of bool [:(X,S,M),ExtREAL:]
[:(X,S,M),ExtREAL:] is non empty V67() set
bool [:(X,S,M),ExtREAL:] is non empty set
A is Element of bool X
B is set
(X,S,M) . B is ext-real Element of ExtREAL
B2 is set
M . B2 is ext-real Element of ExtREAL
C2 is (X,S,M)
B2 \/ C2 is set
C2 is (X,S,M)
B2 \/ C2 is set
C2 is (X,S,M)
B2 \/ C2 is set
A /\ B2 is Element of bool X
A /\ C2 is Element of bool X
(A /\ B2) \/ (A /\ C2) is Element of bool X
D2 is set
M . D2 is ext-real Element of ExtREAL
B2 \/ D2 is set
M . (B2 \/ D2) is ext-real Element of ExtREAL
B2 is Element of S
D2 is Element of S
B2 \/ D2 is Element of S
M . (B2 \/ D2) is ext-real Element of ExtREAL
0. + 0. is V22() V23() ext-real Element of ExtREAL
K56(0.,0.) is V22() V23() ext-real set
O1 is Element of S
M . O1 is ext-real Element of ExtREAL
B2 is set
M . B2 is ext-real Element of ExtREAL
A /\ (B2 \/ C2) is Element of bool X
{} \/ ((A /\ B2) \/ (A /\ C2)) is set
B2 is set
C2 is (X,S,M)
B2 \/ C2 is set