:: 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

bool F

bool (bool F

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