:: 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
bool REAL is non empty cup-closed cap-closed diff-closed preBoolean set
ExtREAL is non empty V62() set
[:NAT,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:NAT,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
bool ExtREAL is non empty cup-closed cap-closed diff-closed preBoolean set
NAT is non empty V27() V28() V29() V61() V62() V63() V64() V65() V66() V67() set
bool NAT is non empty cup-closed cap-closed diff-closed preBoolean set
[:NAT,REAL:] is Relation-like non empty complex-valued ext-real-valued real-valued set
bool [:NAT,REAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool REAL) is non empty cup-closed cap-closed diff-closed preBoolean set
bool NAT is non empty cup-closed cap-closed diff-closed preBoolean set
RAT is non empty V39() V61() V62() V63() V64() V67() set
INT is non empty V39() V61() V62() V63() V64() V65() V67() set
{} is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued set
the Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued set is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued set
1 is non empty V27() V28() V29() V33() V34() V35() ext-real positive V61() V62() V63() V64() V65() V66() Element of NAT
0 is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued Element of NAT
{{}} is functional non empty V61() V62() V63() V64() V65() V66() set
0. is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() ext-real V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued Element of ExtREAL
+infty is 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 {{}} is set
(union {X,S}) \/ (union {{}}) is set
(union {X,S}) \/ {} is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool X
M is Element of bool X
{S,M} is non empty set
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
B is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
B is set
F₁() is set
bool F₁() is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool F₁()) is non empty cup-closed cap-closed diff-closed preBoolean set
bool F₁() is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool F₁())
X is set
S is set
M is set
S is non empty Element of bool (bool F₁())
M is set
A is set
M is set
A is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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 (COMPLEMENT S) is Element of bool X
X \ (union (COMPLEMENT S)) is Element of bool X
union S is Element of bool X
meet (COMPLEMENT S) is Element of bool X
X \ (meet (COMPLEMENT S)) 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool (bool X)
M is set
A is set
M \ A is Element of bool M
bool M is non empty cup-closed cap-closed diff-closed preBoolean set
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
M is set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
A is set
M \ A is Element of bool M
bool M is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
M is set
bool M is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool M) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
A is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool M)
X is non empty set
[:X,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
S is Relation-like X -defined ExtREAL -valued Function-like non empty V14(X) V18(X, ExtREAL ) ext-real-valued Element of bool [:X,ExtREAL:]
M is Element of X
S . M is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
S --> 0. is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:S,ExtREAL:]
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued Element of bool [:S,ExtREAL:]
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
M . {} is ext-real Element of ExtREAL
A is Element of S
M . A is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
+infty is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
the non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
M is Element of S
A is Element of S
M /\ A is set
M \ A is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
M is set
bool M is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool M) is non empty cup-closed cap-closed diff-closed preBoolean set
B is set
bool B is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool B) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
A is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool M)
A is set
B is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool B)
B is set
B \ A is Element of bool B
A \/ B is set
A /\ B is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
A is Element of S
M . A is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
0. + 0. is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool X
{S} is non empty set
NAT --> S is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
rng (NAT --> S) is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
{X} is non empty set
[:NAT,{X}:] is Relation-like non empty set
bool [:NAT,{X}:] is non empty cup-closed cap-closed diff-closed preBoolean set
NAT --> X is Relation-like NAT -defined {X} -valued Function-like non empty V14( NAT ) V18( NAT ,{X}) Element of bool [:NAT,{X}:]
S is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
(NAT --> X) . S is Element of {X}
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool (bool X)
{} X is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued Element of bool X
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean 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
(S,M) followed_by A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
rng ((S,M) followed_by A) is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
((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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool X
M is Element of bool X
{S,M,{}} is non empty set
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
{} X is Relation-like non-empty empty-yielding RAT -valued Function-like one-to-one constant functional empty V27() V28() V29() V31() V32() V33() V61() V62() V63() V64() V65() V66() V67() complex-valued ext-real-valued real-valued natural-valued Element of bool X
{S,M,({} X)} is non empty set
A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng A is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
A . 0 is M7(X, bool X)
A . 1 is M7(X, bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool X
M is Element of bool X
{S,M} is non empty set
S followed_by M is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
rng (S followed_by M) is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
(S followed_by M) . 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
(S followed_by M) . A is M7(X, bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is Element of bool X
M is Element of bool X
{S,M} is non empty set
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng A is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
A . 0 is M7(X, bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty V53() Element of bool (bool X)
COMPLEMENT S is non empty Element of bool (bool X)
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng M is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
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,(COMPLEMENT S):] is Relation-like non empty set
bool [:NAT,(COMPLEMENT S):] is non empty cup-closed cap-closed diff-closed preBoolean set
dom M is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
A is Relation-like NAT -defined COMPLEMENT S -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEMENT S) Element of bool [:NAT,(COMPLEMENT S):]
A is Relation-like NAT -defined COMPLEMENT S -valued Function-like non empty V14( NAT ) V18( NAT , COMPLEMENT S) Element of bool [:NAT,(COMPLEMENT S):]
dom A is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
rng A is non empty Element of bool (COMPLEMENT S)
bool (COMPLEMENT S) is non empty cup-closed cap-closed diff-closed preBoolean set
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
B is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng B is non empty Element of bool (bool X)
A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng A is non empty Element of bool (bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng A is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
Complement A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
B is V27() V28() V29() V33() set
(Complement A) . 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)
(Complement A) . B is M7(X, bool X)
(A . B) ` is Element of bool X
X \ (A . B) is set
rng (Complement A) is non empty Element of bool (bool X)
Intersection (Complement A) is Element of bool X
Complement (Complement A) is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
Union (Complement (Complement A)) is Element of bool X
(Union (Complement (Complement A))) ` is Element of bool X
X \ (Union (Complement (Complement A))) is set
(Intersection (Complement A)) ` is Element of bool X
X \ (Intersection (Complement A)) is set
S is Element of bool (bool X)
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
rng M is non empty set
Intersection M is Element of bool X
Complement M is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
Union (Complement M) is Element of bool X
(Union (Complement M)) ` is Element of bool X
X \ (Union (Complement M)) is set
rng M is non empty Element of bool (bool X)
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
dom (Complement M) is non empty V61() V62() V63() V64() V65() V66() Element of bool NAT
rng (Complement M) is non empty Element of bool (bool X)
A is non empty V53() Element of bool (bool X)
B is set
B is set
(Complement M) . 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
(union A) ` is Element of bool X
X \ (union A) is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean 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 (COMPLEMENT M) is Element of bool X
X \ (meet (COMPLEMENT M)) is Element of bool X
M is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (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 (COMPLEMENT M) is Element of bool X
X \ (union (COMPLEMENT M)) 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,S:] is Relation-like non empty set
bool [:NAT,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
[:NAT,{{}}:] is Relation-like RAT -valued INT -valued non empty complex-valued ext-real-valued real-valued natural-valued set
bool [:NAT,{{}}:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like NAT -defined {{}} -valued Function-like non empty V14( NAT ) V18( NAT ,{{}}) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,{{}}:]
A is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) Element of bool [:NAT,S:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,S:] is Relation-like non empty set
bool [:NAT,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) Element of bool [:NAT,S:]
rng M is non empty set
rng M is non empty Element of bool S
bool S is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,S:] is Relation-like non empty set
bool [:NAT,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) Element of bool [:NAT,S:]
(X,S,M) is non empty Element of bool (bool X)
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A) is non empty Element of bool (bool X)
A is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
(X,(bool X),A) is non empty Element of bool (bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,S:] is Relation-like non empty set
bool [:NAT,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) Element of bool [:NAT,S:]
(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
bool [:X,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like X -defined S -valued Function-like non empty V14(X) V18(X,S) Element of bool [:X,S:]
A is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued Element of bool [:S,ExtREAL:]
A * M is Relation-like X -defined ExtREAL -valued Function-like non empty V14(X) V18(X, ExtREAL ) ext-real-valued Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:X,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
B is Element of X
(A * M) . B is ext-real Element of ExtREAL
dom (A * M) is non empty Element of bool X
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
M . B is Element of S
A . (M . B) is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is ext-real Element of ExtREAL
A is ext-real Element of ExtREAL
B is set
B is set
B is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued Element of bool [:S,ExtREAL:]
B is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued Element of bool [:S,ExtREAL:]
A is Element of S
M . A is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued Element of bool [:S,ExtREAL:]
A is Element of S
M . A is ext-real Element of ExtREAL
[:NAT,S:] is Relation-like non empty set
bool [:NAT,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
A is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) disjoint_valued Element of bool [:NAT,S:]
M * A is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) V18( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
SUM (M * A) is ext-real Element of ExtREAL
Ser (M * A) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) V18( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,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
M . {} is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty Element of bool (bool X)
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:NAT,(bool X):] is Relation-like non empty set
bool [:NAT,(bool X):] is non empty cup-closed cap-closed diff-closed preBoolean set
A is Element of bool X
B is Element of bool X
{A,B,{}} is non empty set
F is Relation-like NAT -defined bool X -valued Function-like non empty V14( NAT ) V18( NAT , bool X) Element of bool [:NAT,(bool X):]
(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
bool [:NAT,S:] is non empty cup-closed cap-closed diff-closed preBoolean set
F is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) Element of bool [:NAT,S:]
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
F is Relation-like NAT -defined S -valued Function-like non empty V14( NAT ) V18( NAT ,S) disjoint_valued Element of bool [:NAT,S:]
(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 is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) V18( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
(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
M . {} is ext-real Element of ExtREAL
0 + 1 is V27() V28() V29() V33() V34() V35() ext-real V61() V62() V63() V64() V65() V66() Element of NAT
Ser (M * F) is Relation-like NAT -defined ExtREAL -valued Function-like non empty V14( NAT ) V18( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]
(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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
M is set
bool M is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool M) is non empty cup-closed cap-closed diff-closed preBoolean set
B is set
bool B is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool B) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
A is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (M) Element of bool (bool M)
A is set
B is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (B) Element of bool (bool B)
B is set
B \ A is Element of bool B
A \/ B is set
A /\ B is set
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean 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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
A is Element of S
M . A is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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
0. + 0. is ext-real Element of ExtREAL
X is set
bool X is non empty cup-closed cap-closed diff-closed preBoolean set
bool (bool X) is non empty cup-closed cap-closed diff-closed preBoolean set
S is non empty cup-closed cap-closed diff-closed preBoolean compl-closed sigma-multiplicative (X) Element of bool (bool X)
[:S,ExtREAL:] is Relation-like non empty ext-real-valued set
bool [:S,ExtREAL:] is non empty cup-closed cap-closed diff-closed preBoolean set
M is Relation-like S -defined ExtREAL -valued Function-like non empty V14(S) V18(S, ExtREAL ) ext-real-valued zeroed nonnegative (X,S) Element of bool [:S,ExtREAL:]
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