:: MEASURE1 semantic presentation

REAL is non empty V39() V61() V62() V63() V67() set
NAT is non empty V27() V28() V29() V61() V62() V63() V64() V65() V66() V67() Element of bool REAL

ExtREAL is non empty V62() set

NAT is non empty V27() V28() V29() V61() V62() V63() V64() V65() V66() V67() set

RAT is non empty V39() V61() V62() V63() V64() V67() set
INT is non empty V39() V61() V62() V63() V64() V65() V67() set

1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive V61() V62() V63() V64() V65() V66() Element of NAT

is functional non empty V61() V62() V63() V64() V65() V66() set

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

(union {X,S}) \/ () is set
(union {X,S}) \/ {} is set
X is set

S is Element of bool X
M is Element of bool X
{S,M} is non empty set

B is set
X is set

S is Element of bool X
M is Element of bool X
A is Element of bool X
{S,M,A} is non empty set

B is set
F1() is set

bool (bool F1()) is non empty cup-closed cap-closed diff-closed preBoolean set

X is set
S is set
M is set
S is non empty Element of bool (bool F1())
M is set
A is set
M is set
A is set
X is set

X is set

S is non empty Element of bool (bool X)
COMPLEMENT S is Element of bool (bool X)
M is Element of bool X
M ` is Element of bool X
X \ M is set
(M `) ` is Element of bool X
X \ (M `) is set
X is set

S is non empty Element of bool (bool X)
meet S is Element of bool X
COMPLEMENT S is non empty Element of bool (bool X)
union () is Element of bool X
X \ (union ()) is Element of bool X
union S is Element of bool X
meet () is Element of bool X
X \ (meet ()) is Element of bool X
M is set
A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
(B `) ` is Element of bool X
X \ (B `) is set
M is set
A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
M is set
A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
(B `) ` is Element of bool X
X \ (B `) is set
M is set
A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
X is set

S is Element of bool (bool X)
M is set
A is Element of bool X
A ` is Element of bool X
X \ A is set
X \ M is Element of bool X
M is Element of bool X
M ` is Element of bool X
X \ M is set
X is set

S is Element of bool (bool X)
M is set
A is set
M /\ A is set
X \ M is Element of bool X
X \ A is Element of bool X
(X \ M) \/ (X \ A) is Element of bool X
X /\ (M /\ A) is set
X \ (M /\ A) is Element of bool X
X \ (X \ (M /\ A)) is Element of bool X
X \ ((X \ M) \/ (X \ A)) is Element of bool X
S is Element of bool (bool X)
M is set
A is set
M \/ A is set
X \ M is Element of bool X
X \ A is Element of bool X
(X \ M) /\ (X \ A) is Element of bool X
X /\ (M \/ A) is set
X \ (M \/ A) is Element of bool X
X \ (X \ (M \/ A)) is Element of bool X
X \ ((X \ M) /\ (X \ A)) is Element of bool X
X is set

S is non empty cup-closed cap-closed compl-closed Element of bool (bool X)
COMPLEMENT S is non empty Element of bool (bool X)
M is set
A is Element of bool X
A ` is Element of bool X
X \ A is set
A is Element of bool X
A ` is Element of bool X
X \ A is set
(A `) ` is Element of bool X
X \ (A `) is set
X is set

S is Element of bool (bool X)
M is set
A is set
M \ A is Element of bool M

X \ A is Element of bool X
M /\ (X \ A) is Element of bool X
M /\ X is set
(M /\ X) \ A is Element of bool (M /\ X)
bool (M /\ X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set

M is set

A is set
M \ A is Element of bool M

X is set

M is set

X is non empty set

M is Element of X
S . M is ext-real Element of ExtREAL
X is set

X is set

A is Element of S
B is Element of S
A \/ B is Element of S
M . (A \/ B) is ext-real Element of ExtREAL
M . A is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
(M . A) + (M . B) is ext-real Element of ExtREAL
B is set
A is set
B is Element of S
M . B is ext-real Element of ExtREAL
F is Element of S
M . F is ext-real Element of ExtREAL
(M . B) + (M . F) is ext-real Element of ExtREAL

A is Element of S
M . A is ext-real Element of ExtREAL
X is set

X is set

A is Element of S
B is Element of S
M . A is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
B \ A is Element of S
B is Element of S
M . B is ext-real Element of ExtREAL
A \/ B is Element of S
M . (A \/ B) is ext-real Element of ExtREAL
(M . A) + (M . B) is ext-real Element of ExtREAL

X is set

A is Element of S
B is Element of S
M . A is ext-real Element of ExtREAL
B \ A is Element of S
M . (B \ A) is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
(M . B) - (M . A) is ext-real Element of ExtREAL
K209((M . A)) is ext-real set
K208((M . B),K209((M . A))) is ext-real set
A \/ (B \ A) is Element of S
M . (A \/ (B \ A)) is ext-real Element of ExtREAL
(M . A) + (M . (B \ A)) is ext-real Element of ExtREAL
X is set

X is set

S is non empty cup-closed Element of bool (bool X)
M is Element of S
A is Element of S
M \/ A is set
X is set

M is Element of S
A is Element of S
M /\ A is set
M \ A is set
X is set

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

M is set

B is set

A is set

B is set
B \ A is Element of bool B
A \/ B is set
A /\ B is set
X is set

A is Element of S
M . A is ext-real Element of ExtREAL
X is set

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

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

X is set

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

[:NAT,(bool X):] is Relation-like non empty set

S is Element of bool X
{S} is non empty set

[:NAT,(bool X):] is Relation-like non empty set

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

X is set
{X} is non empty set

S is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
() . S is Element of {X}
X is set

S is Element of bool (bool X)

[:NAT,(bool X):] is Relation-like non empty set

X is set

[:NAT,(bool X):] is Relation-like non empty set

S is Element of bool X
M is Element of bool X
A is Element of bool X
{S,M,A} is non empty set

[:NAT,(bool X):] is Relation-like non empty set

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

((S,M) followed_by A) . 0 is M7(X, bool X)
((S,M) followed_by A) . 1 is M7(X, bool X)
B is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
((S,M) followed_by A) . B is M7(X, bool X)
X is set

S is Element of bool X
M is Element of bool X
{S,M,{}} is non empty set

[:NAT,(bool X):] is Relation-like non empty set

{S,M,({} X)} is non empty set

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

A . 0 is M7(X, bool X)
A . 1 is M7(X, bool X)
X is set

[:NAT,(bool X):] is Relation-like non empty set

S is Element of bool X
M is Element of bool X
{S,M} is non empty set

[:NAT,(bool X):] is Relation-like non empty set

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

() . 0 is M7(X, bool X)
A is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
() . A is M7(X, bool X)
X is set

S is Element of bool X
M is Element of bool X
{S,M} is non empty set

[:NAT,(bool X):] is Relation-like non empty set

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

A . 0 is M7(X, bool X)
X is set

S is non empty V53() Element of bool (bool X)
COMPLEMENT S is non empty Element of bool (bool X)

[:NAT,(bool X):] is Relation-like non empty set

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

A is set
M . A is set
B is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
(B `) ` is Element of bool X
X \ (B `) is set
[:NAT,():] is Relation-like non empty set

dom M is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT

dom A is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
rng A is non empty Element of bool ()

B is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
A is set
M . A is set
A . A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set

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

rng A is non empty Element of bool (bool X)
X is set

X is set

{{},X} is non empty cap-closed set
S is non empty Element of bool (bool X)
M is set
X \ M is Element of bool X
M is non empty V53() Element of bool (bool X)
union M is Element of bool X
A is set
X is set

S is Element of bool (bool X)
M is non empty V53() Element of bool (bool X)
union M is Element of bool X

[:NAT,(bool X):] is Relation-like non empty set

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

B is V27() V28() V29() V33() set
() . B is Element of bool X
B is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
A . B is M7(X, bool X)
() . B is M7(X, bool X)
(A . B) ` is Element of bool X
X \ (A . B) is set
rng () is non empty Element of bool (bool X)
Intersection () is Element of bool X

Union () is Element of bool X
(Union ()) ` is Element of bool X
X \ (Union ()) is set
() ` is Element of bool X
X \ () is set
S is Element of bool (bool X)

[:NAT,(bool X):] is Relation-like non empty set

rng M is non empty set
Intersection M is Element of bool X

Union () is Element of bool X
(Union ()) ` is Element of bool X
X \ (Union ()) is set
rng M is non empty Element of bool (bool X)

dom () is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
rng () is non empty Element of bool (bool X)
A is non empty V53() Element of bool (bool X)
B is set
B is set
() . B is set
A is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
M . A is M7(X, bool X)
(M . A) ` is Element of bool X
X \ (M . A) is set
union A is Element of bool X
() ` is Element of bool X
X \ () is set
X is set

X is set

S is non empty Element of bool (bool X)
M is non empty V53() Element of bool (bool X)
union M is Element of bool X
COMPLEMENT M is non empty Element of bool (bool X)
A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
(B `) ` is Element of bool X
X \ (B `) is set
meet () is Element of bool X
X \ (meet ()) is Element of bool X

M is non empty V53() Element of bool (bool X)
meet M is Element of bool X
COMPLEMENT M is non empty Element of bool (bool X)
A is set
B is Element of bool X
B ` is Element of bool X
X \ B is set
(B `) ` is Element of bool X
X \ (B `) is set
union () is Element of bool X
X \ (union ()) is Element of bool X
M is set
X \ M is Element of bool X
A is non empty V53() Element of bool (bool X)
meet A is Element of bool X
X is set

[:NAT,S:] is Relation-like non empty set

B is set
A . B is set
dom A is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
dom A is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
dom A is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
B is set
B is set
A . B is set
A . B is set
X is set

X is set

[:NAT,S:] is Relation-like non empty set

rng M is non empty set
rng M is non empty Element of bool S

X is set

[:NAT,S:] is Relation-like non empty set

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

[:NAT,(bool X):] is Relation-like non empty set

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

(X,(bool X),A) is non empty Element of bool (bool X)
X is set

[:NAT,S:] is Relation-like non empty set

(X,S,M) is non empty Element of bool (bool X)
union (X,S,M) is Element of bool X
X is non empty set
S is non empty set
[:X,S:] is Relation-like non empty set

M is Relation-like X -defined S -valued Function-like non empty V14(X) V18(X,S) Element of bool [:X,S:]

B is Element of X
(A * M) . B is ext-real Element of ExtREAL
dom (A * M) is non empty Element of bool X

M . B is Element of S
A . (M . B) is ext-real Element of ExtREAL
X is set

B is set
B is set

B is Element of S
B . B is ext-real Element of ExtREAL
A is Element of S
B . A is ext-real Element of ExtREAL
X is set

X is set

A is Element of S
M . A is ext-real Element of ExtREAL
X is set

X is set

A is Element of S
M . A is ext-real Element of ExtREAL
[:NAT,S:] is Relation-like non empty set

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

rng (Ser (M * A)) is non empty V53() V62() Element of bool ExtREAL
K248((rng (Ser (M * A)))) is ext-real Element of ExtREAL
(X,S,A) is non empty Element of bool (bool X)
union (X,S,A) is Element of bool X
M . (union (X,S,A)) is ext-real Element of ExtREAL
B is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
(M * A) . B is ext-real Element of ExtREAL
dom (M * A) is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
A . B is Element of S
M . (A . B) 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

X is set

X is set

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

1 + 1 is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
B is Element of S
B is Element of S
(X,S,B,B) is Element of S
M . (X,S,B,B) is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
(M . B) + (M . B) is ext-real Element of ExtREAL

[:NAT,(bool X):] is Relation-like non empty set

A is Element of bool X
B is Element of bool X
{A,B,{}} is non empty set

(X,(bool X),F) is non empty Element of bool (bool X)
F . 0 is M7(X, bool X)
F . 1 is M7(X, bool X)
F is set
[:NAT,S:] is Relation-like non empty set

F is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
H is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
F . F is Element of S
F . H is Element of S
(X,S,(F . F),(F . H)) is Element of S
(X,S,(F . F),(F . H)) is Element of S
(X,S,(F . F),(F . H)) is Element of S
(X,S,(F . F),(F . H)) is Element of S
(X,S,(F . F),(F . H)) is Element of S
F is set
H is set
F . F is set
F . H is set
dom F is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
union {A,B,{}} is set
{A,B} is non empty set
union {A,B} is set

(X,S,F) is non empty Element of bool (bool X)
union (X,S,F) is Element of bool X
A \/ B is Element of bool X

(M * F) . 0 is ext-real Element of ExtREAL
M . A is ext-real Element of ExtREAL
(M * F) . 1 is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
H is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
(M * F) . H is ext-real Element of ExtREAL
y1 is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
(M * F) . y1 is ext-real Element of ExtREAL
F . y1 is Element of S
M . (F . y1) is ext-real Element of ExtREAL
dom (M * F) is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
F . H is Element of S

0 + 1 is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT

(Ser (M * F)) . 1 is ext-real Element of ExtREAL
(Ser (M * F)) . (1 + 1) is ext-real Element of ExtREAL
(M * F) . (1 + 1) is ext-real Element of ExtREAL
((Ser (M * F)) . 1) + ((M * F) . (1 + 1)) is ext-real Element of ExtREAL
((Ser (M * F)) . 1) + 0. is ext-real Element of ExtREAL
(Ser (M * F)) . 0 is ext-real Element of ExtREAL
((Ser (M * F)) . 0) + ((M * F) . 1) is ext-real Element of ExtREAL
A is Element of S
M . A is ext-real Element of ExtREAL
B is Element of S
M . B is ext-real Element of ExtREAL
(M . A) + (M . B) is ext-real Element of ExtREAL
SUM (M * F) is ext-real Element of ExtREAL
rng (Ser (M * F)) is non empty V53() V62() Element of bool ExtREAL
K248((rng (Ser (M * F)))) is ext-real Element of ExtREAL
X is set

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

A is Element of S
B is Element of S
M . A is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
X is set

A is Element of S
B is Element of S
M . A is ext-real Element of ExtREAL
(X,S,B,A) is Element of S
M . (X,S,B,A) is ext-real Element of ExtREAL
M . B is ext-real Element of ExtREAL
(M . B) - (M . A) is ext-real Element of ExtREAL
K209((M . A)) is ext-real set
K208((M . B),K209((M . A))) is ext-real set
X is set

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

M is set

B is set

A is set

B is set
B \ A is Element of bool B
A \/ B is set
A /\ B is set
X is set

A is non empty V53() Element of bool (bool X)
union A is Element of bool X
meet A is Element of bool X
B is set
X is set

A is Element of S
M . A is ext-real Element of ExtREAL
X is set

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

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

X is set

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