:: MEASURE4 semantic presentation

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

NAT is non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() Element of bool REAL

bool REAL is non empty set

ExtREAL is non empty V60() set

[:NAT,ExtREAL:] is non empty ext-real-valued set

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

bool ExtREAL is non empty set

NAT is non empty V15() V16() V17() V59() V60() V61() V62() V63() V64() V65() set

bool NAT is non empty set

[:NAT,REAL:] is non empty complex-valued ext-real-valued real-valued set

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

bool (bool REAL) is non empty set

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

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

{} is empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set

the empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set is empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() set

0 is empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() Element of NAT

1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

0. is empty V15() V16() V17() V19() V20() V21() V22() real ext-real non positive non negative V59() V60() V61() V62() V63() V64() V65() Element of ExtREAL

+infty is non empty non real ext-real positive non negative set

-infty is non empty non real ext-real non positive negative set

{+infty,-infty} is non empty V60() set

REAL \/ {+infty,-infty} is non empty V60() set

X is set

bool X is non empty set

bool (bool X) is non empty set

C is non empty Element of bool (bool X)

[:NAT,C:] is non empty set

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

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

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

rng B is Element of bool C

bool C is non empty set

union (rng B) is set

rng A is Element of bool C

union (rng A) is set

B is Element of C

B /\ (union (rng A)) is Element of bool X

F9 is set

a is set

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

bool NAT is non empty set

b is set

B . b is set

F is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

A . F is Element of C

B /\ (A . F) is Element of bool X

F9 is set

a is set

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

bool NAT is non empty set

b is set

A . b is set

F is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . F is Element of C

B /\ a is Element of bool X

X is set

bool X is non empty set

bool (bool X) is non empty set

C is non empty Element of bool (bool X)

[:NAT,C:] is non empty set

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

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

B . 0 is Element of C

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

A . 0 is Element of C

rng A is Element of bool C

bool C is non empty set

union (rng A) is set

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

B . 0 is Element of C

rng B is Element of bool C

union (rng B) is set

F9 is set

a is set

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

bool NAT is non empty set

b is set

A . b is set

b is V15() V16() V17() V21() V22() real ext-real non negative set

A . b is Element of C

b is V15() V16() V17() V21() V22() real ext-real non negative set

A . b is Element of C

F is V15() V16() V17() V21() V22() real ext-real non negative set

F + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . b is Element of C

Q is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . Q is Element of C

QQ is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

A . QQ is Element of C

Q + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . (Q + 1) is Element of C

A . (Q + 1) is Element of C

(A . (Q + 1)) \ (B . Q) is Element of bool (A . (Q + 1))

bool (A . (Q + 1)) is non empty set

F is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . F is Element of C

Q is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . Q is Element of C

b is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . b is Element of C

b is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . b is Element of C

F9 is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . F9 is Element of C

A . F9 is Element of C

a is V15() V16() V17() V21() V22() real ext-real non negative set

a + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

b is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . b is Element of C

(A . F9) \ (B . b) is Element of bool (A . F9)

bool (A . F9) is non empty set

F9 is set

a is set

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

bool NAT is non empty set

b is set

B . b is set

F is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

A . F is Element of C

X is set

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

bool X is non empty set

bool (bool X) is non empty set

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

union C is Element of bool X

A is set

X \ A is Element of bool X

C is Element of bool (bool X)

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

X is set

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

bool X is non empty set

bool (bool X) is non empty set

[:(bool X),ExtREAL:] is non empty ext-real-valued set

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

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

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

(bool X) --> 0. is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:(bool X),ExtREAL:]

A is Element of bool X

((bool X) --> 0.) . A is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

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

rng A is Element of bool (bool X)

bool (bool X) is non empty set

union (rng A) is Element of bool X

((bool X) --> 0.) . (union (rng A)) is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

((bool X) --> 0.) * A is V1() V4( NAT ) V5( ExtREAL ) V5( RAT ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,ExtREAL:]

SUM (((bool X) --> 0.) * A) is ext-real Element of ExtREAL

B is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

(((bool X) --> 0.) * A) . B is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

dom (((bool X) --> 0.) * A) is V59() V60() V61() V62() V63() V64() Element of bool NAT

bool NAT is non empty set

A . B is Element of bool X

((bool X) --> 0.) . (A . B) is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

Ser (((bool X) --> 0.) * A) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(Ser (((bool X) --> 0.) * A)) . 0 is ext-real Element of ExtREAL

(((bool X) --> 0.) * A) . 0 is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

((bool X) --> 0.) . {} is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

A is Element of bool X

B is Element of bool X

((bool X) --> 0.) . A is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

((bool X) --> 0.) . B is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

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

rng B is Element of bool (bool X)

bool (bool X) is non empty set

union (rng B) is Element of bool X

((bool X) --> 0.) . (union (rng B)) is V15() V16() V17() V21() V22() real ext-real non negative Element of ExtREAL

((bool X) --> 0.) * B is V1() V4( NAT ) V5( ExtREAL ) V5( RAT ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) complex-valued ext-real-valued real-valued natural-valued Element of bool [:NAT,ExtREAL:]

SUM (((bool X) --> 0.) * B) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

B is set

B is set

X \ B is Element of bool X

F9 is Element of bool X

a is Element of bool X

C . F9 is ext-real Element of ExtREAL

C . a is ext-real Element of ExtREAL

(C . F9) + (C . a) is ext-real Element of ExtREAL

F9 \/ a is Element of bool X

C . (F9 \/ a) is ext-real Element of ExtREAL

b is set

F is Element of bool X

Q is Element of bool X

X \ b is Element of bool X

C . F is ext-real Element of ExtREAL

C . Q is ext-real Element of ExtREAL

(C . F) + (C . Q) is ext-real Element of ExtREAL

F \/ Q is Element of bool X

C . (F \/ Q) is ext-real Element of ExtREAL

F9 is Element of bool X

a is Element of bool X

C . F9 is ext-real Element of ExtREAL

C . a is ext-real Element of ExtREAL

(C . F9) + (C . a) is ext-real Element of ExtREAL

F9 \/ a is Element of bool X

C . (F9 \/ a) is ext-real Element of ExtREAL

b is set

F is Element of bool X

Q is Element of bool X

X \ b is Element of bool X

C . F is ext-real Element of ExtREAL

C . Q is ext-real Element of ExtREAL

(C . F) + (C . Q) is ext-real Element of ExtREAL

F \/ Q is Element of bool X

C . (F \/ Q) is ext-real Element of ExtREAL

QQ is Element of bool X

Q is Element of bool X

C . QQ is ext-real Element of ExtREAL

C . Q is ext-real Element of ExtREAL

(C . QQ) + (C . Q) is ext-real Element of ExtREAL

QQ \/ Q is Element of bool X

C . (QQ \/ Q) is ext-real Element of ExtREAL

B is set

B is Element of bool X

A is Element of bool X

F9 is Element of bool X

X \ A is Element of bool X

C . B is ext-real Element of ExtREAL

C . F9 is ext-real Element of ExtREAL

(C . B) + (C . F9) is ext-real Element of ExtREAL

B \/ F9 is Element of bool X

C . (B \/ F9) is ext-real Element of ExtREAL

B is non empty Element of bool (bool X)

F9 is Element of bool X

a is Element of bool X

b is Element of bool X

X \ F9 is Element of bool X

C . a is ext-real Element of ExtREAL

C . b is ext-real Element of ExtREAL

(C . a) + (C . b) is ext-real Element of ExtREAL

a \/ b is Element of bool X

C . (a \/ b) is ext-real Element of ExtREAL

F is Element of bool X

X \ F is Element of bool X

A is non empty Element of bool (bool X)

B is non empty Element of bool (bool X)

B is set

F9 is Element of bool X

X \ F9 is Element of bool X

a is Element of bool X

b is Element of bool X

C . a is ext-real Element of ExtREAL

C . b is ext-real Element of ExtREAL

(C . a) + (C . b) is ext-real Element of ExtREAL

a \/ b is Element of bool X

C . (a \/ b) is ext-real Element of ExtREAL

F9 is Element of bool X

X \ F9 is Element of bool X

a is Element of bool X

b is Element of bool X

C . a is ext-real Element of ExtREAL

C . b is ext-real Element of ExtREAL

(C . a) + (C . b) is ext-real Element of ExtREAL

a \/ b is Element of bool X

C . (a \/ b) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

A is Element of bool X

B is Element of bool X

A \/ B is Element of bool X

C . (A \/ B) is ext-real Element of ExtREAL

C . A is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C . A) + (C . B) is ext-real Element of ExtREAL

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

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

B is Element of bool X

{A,B,B} is non empty set

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

rng F9 is Element of bool (bool X)

bool (bool X) is non empty set

F9 . 0 is Element of bool X

F9 . 1 is Element of bool X

C * F9 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(C * F9) . 1 is ext-real Element of ExtREAL

union {A,B,B} is set

b is set

F is set

b is set

F is Element of bool X

F is Element of bool X

F is Element of bool X

2 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

b is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

(C * F9) . b is ext-real Element of ExtREAL

1 + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

F9 . b is Element of bool X

C . (F9 . b) is ext-real Element of ExtREAL

F9 . 2 is Element of bool X

(C * F9) . 2 is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C * F9) . 0 is ext-real Element of ExtREAL

Ser (C * F9) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(Ser (C * F9)) . 1 is ext-real Element of ExtREAL

(Ser (C * F9)) . 0 is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

F is ext-real Element of ExtREAL

(Ser (C * F9)) . 2 is ext-real Element of ExtREAL

1 + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

(C * F9) . (1 + 1) is ext-real Element of ExtREAL

b + ((C * F9) . (1 + 1)) is ext-real Element of ExtREAL

((Ser (C * F9)) . 1) + 0. is ext-real Element of ExtREAL

0 + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

(C * F9) . (0 + 1) is ext-real Element of ExtREAL

F + ((C * F9) . (0 + 1)) is ext-real Element of ExtREAL

SUM (C * F9) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

A is Element of bool X

X \ A is Element of bool X

B is Element of bool X

B is Element of bool X

B \/ B is Element of bool X

C . (B \/ B) is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C . B) + (C . B) is ext-real Element of ExtREAL

B is Element of bool X

B is Element of bool X

C . B is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C . B) + (C . B) is ext-real Element of ExtREAL

B \/ B is Element of bool X

C . (B \/ B) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

A is Element of bool X

B is Element of bool X

A \/ B is Element of bool X

C . (A \/ B) is ext-real Element of ExtREAL

C . A is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C . A) + (C . B) is ext-real Element of ExtREAL

B \ A is Element of bool X

X \ A is Element of bool X

X is set

C is set

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

bool C is non empty set

bool (bool C) is non empty set

C \ X is Element of bool C

A is V1() V4( bool C) V5( ExtREAL ) Function-like non empty V14( bool C) V30( bool C, ExtREAL ) ext-real-valued (C)

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

C \ (C \ X) is Element of bool C

B is Element of bool C

B is Element of bool C

A . B is ext-real Element of ExtREAL

A . B is ext-real Element of ExtREAL

(A . B) + (A . B) is ext-real Element of ExtREAL

B \/ B is Element of bool C

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

C /\ X is set

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is set

A is set

C \/ A is set

B is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

B is Element of bool X

F9 is Element of bool X

B \/ F9 is Element of bool X

X \ (B \/ F9) is Element of bool X

b is Element of bool X

F is Element of bool X

B . b is ext-real Element of ExtREAL

B . F is ext-real Element of ExtREAL

(B . b) + (B . F) is ext-real Element of ExtREAL

b \/ F is Element of bool X

B . (b \/ F) is ext-real Element of ExtREAL

b \ B is Element of bool X

(b \ B) \/ F is Element of bool X

X \ B is Element of bool X

X \ F9 is Element of bool X

(X \ B) /\ (X \ F9) is Element of bool X

b /\ B is Element of bool X

(b /\ B) \/ (b \ B) is Element of bool X

B . (b /\ B) is ext-real Element of ExtREAL

B . (b \ B) is ext-real Element of ExtREAL

(B . (b /\ B)) + (B . (b \ B)) is ext-real Element of ExtREAL

((B . (b /\ B)) + (B . (b \ B))) + (B . F) is ext-real Element of ExtREAL

F9 \/ B is Element of bool X

(F9 \/ B) \ B is Element of bool X

F9 \ B is Element of bool X

(B . (b \ B)) + (B . F) is ext-real Element of ExtREAL

B . ((b \ B) \/ F) is ext-real Element of ExtREAL

(X \ B) \/ F is Element of bool X

((b /\ B) \/ (b \ B)) \/ F is Element of bool X

B . (((b /\ B) \/ (b \ B)) \/ F) is ext-real Element of ExtREAL

(b /\ B) \/ ((b \ B) \/ F) is Element of bool X

B . ((b /\ B) \/ ((b \ B) \/ F)) is ext-real Element of ExtREAL

(B . (b /\ B)) + (B . ((b \ B) \/ F)) is ext-real Element of ExtREAL

(B . (b /\ B)) + ((B . (b \ B)) + (B . F)) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is set

A is set

C /\ A is set

B is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

X \ A is Element of bool X

X /\ X is set

X /\ (C /\ A) is set

X \ (C /\ A) is Element of bool X

X \ (X \ (C /\ A)) is Element of bool X

X \ C is Element of bool X

(X \ C) \/ (X \ A) is Element of bool X

X \ ((X \ C) \/ (X \ A)) is Element of bool X

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is set

A is set

C \ A is Element of bool C

bool C is non empty set

B is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

X \ A is Element of bool X

C /\ (X \ A) is Element of bool X

B is set

X is set

bool X is non empty set

bool (bool X) is non empty set

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

[:NAT,C:] is non empty set

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

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

B is Element of C

B is set

A . B is set

B /\ (A . B) is Element of bool X

F9 is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

A . F9 is Element of C

B /\ (A . F9) is Element of C

a is set

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

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

F9 is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

B . F9 is Element of C

A . F9 is Element of C

B /\ (A . F9) is Element of C

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

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

union A is Element of bool X

X \ (union A) is Element of bool X

B is Element of bool X

F9 is Element of bool X

C . B is ext-real Element of ExtREAL

C . F9 is ext-real Element of ExtREAL

(C . B) + (C . F9) is ext-real Element of ExtREAL

B \/ F9 is Element of bool X

C . (B \/ F9) is ext-real Element of ExtREAL

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

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

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

rng a is Element of bool (bool X)

bool (bool X) is non empty set

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

[:NAT,B:] is non empty set

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

a . 0 is Element of bool X

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

b . 0 is Element of B

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

F . 0 is Element of B

union (rng a) is Element of bool X

rng F is non empty V47() N_Sub_fam of B

union (rng F) is Element of bool X

Q is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

a . Q is Element of bool X

Q is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

b . Q is Element of B

Q + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

b . (Q + 1) is Element of B

a . (Q + 1) is Element of bool X

(a . (Q + 1)) \/ (b . Q) is set

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

rng Q is non empty V47() N_Sub_fam of B

union (rng Q) is Element of bool X

B /\ (union (rng F)) is Element of bool X

Q . 0 is Element of B

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

QQ . 0 is Element of B

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

F . 0 is Element of bool X

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

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

C * Q is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

Ser (C * Q) is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

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

R is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . R is Element of bool X

F9 \/ (QQ . R) is Element of bool X

C . (F9 \/ (QQ . R)) is ext-real Element of ExtREAL

(Ser (C * Q)) . R is ext-real Element of ExtREAL

(C . F9) + ((Ser (C * Q)) . R) is ext-real Element of ExtREAL

R + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . (R + 1) is Element of bool X

F9 \/ (QQ . (R + 1)) is Element of bool X

C . (F9 \/ (QQ . (R + 1))) is ext-real Element of ExtREAL

(Ser (C * Q)) . (R + 1) is ext-real Element of ExtREAL

(C . F9) + ((Ser (C * Q)) . (R + 1)) is ext-real Element of ExtREAL

F . (R + 1) is Element of bool X

G . R is Element of bool X

(F . (R + 1)) \ (G . R) is Element of bool X

Q . (R + 1) is Element of bool X

(QQ . R) \/ (Q . (R + 1)) is Element of bool X

(C * Q) . (R + 1) is ext-real Element of ExtREAL

QQ . 0 is Element of bool X

B /\ (F . 0) is Element of bool X

G . 0 is Element of bool X

y is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . y is Element of bool X

y + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

F . (y + 1) is Element of bool X

G . y is Element of bool X

(F . (y + 1)) \ (G . y) is Element of bool X

k is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . k is Element of bool X

G . k is Element of bool X

k + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . (k + 1) is Element of bool X

G . (k + 1) is Element of bool X

F . (k + 1) is Element of bool X

B /\ (F . (k + 1)) is Element of bool X

(F . (k + 1)) \ (G . k) is Element of bool X

B /\ ((F . (k + 1)) \ (G . k)) is Element of bool X

Q . (k + 1) is Element of bool X

(Q . (k + 1)) \/ (QQ . k) is Element of bool X

F . (k + 1) is Element of B

B /\ (F . (k + 1)) is Element of bool X

(B /\ (F . (k + 1))) \/ (QQ . k) is Element of bool X

(B /\ ((F . (k + 1)) \ (G . k))) \/ (QQ . k) is Element of bool X

(F . (k + 1)) \/ (G . k) is Element of bool X

(QQ . R) /\ ((F . (R + 1)) \ (G . R)) is Element of bool X

X \ ((F . (R + 1)) \ (G . R)) is Element of bool X

y is set

F . (R + 1) is Element of B

B /\ (F . (R + 1)) is Element of bool X

B /\ ((F . (R + 1)) \ (G . R)) is Element of bool X

rng F is Element of bool (bool X)

union (rng F) is Element of bool X

X \ (union (rng F)) is Element of bool X

C . (Q . (R + 1)) is ext-real Element of ExtREAL

(C . (Q . (R + 1))) + (C . (F9 \/ (QQ . R))) is ext-real Element of ExtREAL

(F9 \/ (QQ . R)) \/ (Q . (R + 1)) is Element of bool X

C . ((F9 \/ (QQ . R)) \/ (Q . (R + 1))) is ext-real Element of ExtREAL

((C . F9) + ((Ser (C * Q)) . R)) + ((C * Q) . (R + 1)) is ext-real Element of ExtREAL

((Ser (C * Q)) . R) + ((C * Q) . (R + 1)) is ext-real Element of ExtREAL

(C . F9) + (((Ser (C * Q)) . R) + ((C * Q) . (R + 1))) is ext-real Element of ExtREAL

QQ . 0 is Element of bool X

B /\ (F . 0) is Element of bool X

(Ser (C * Q)) . 0 is ext-real Element of ExtREAL

(C * Q) . 0 is ext-real Element of ExtREAL

C . (QQ . 0) is ext-real Element of ExtREAL

rng F is Element of bool (bool X)

union (rng F) is Element of bool X

X \ (union (rng F)) is Element of bool X

X \ (F . 0) is Element of bool X

F9 \/ (QQ . 0) is Element of bool X

C . (F9 \/ (QQ . 0)) is ext-real Element of ExtREAL

(C . F9) + ((Ser (C * Q)) . 0) is ext-real Element of ExtREAL

R is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . R is Element of bool X

R + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

QQ . (R + 1) is Element of bool X

F . (R + 1) is Element of B

B /\ (F . (R + 1)) is Element of bool X

Q . (R + 1) is Element of bool X

(Q . (R + 1)) \/ (QQ . R) is Element of bool X

(B /\ (F . (R + 1))) \/ (QQ . R) is Element of bool X

B \/ B is Element of bool X

B /\ (F . 0) is Element of bool X

rng Q is Element of bool (bool X)

union (rng Q) is Element of bool X

F9 \/ B is Element of bool X

C . (F9 \/ B) is ext-real Element of ExtREAL

(C . (F9 \/ B)) - (C . F9) is ext-real Element of ExtREAL

R is set

y is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

k is set

R is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

y is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

R . y is ext-real Element of ExtREAL

-infty is non empty non real ext-real non positive negative Element of ExtREAL

+infty is non empty non real ext-real positive non negative Element of ExtREAL

{-infty,+infty} is non empty V60() set

k is V22() real ext-real Element of REAL

(C . F9) - (C . F9) is ext-real Element of ExtREAL

k - k is V22() real ext-real Element of REAL

y is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (C * Q)) . y is ext-real Element of ExtREAL

QQ . y is Element of bool X

F9 \/ (QQ . y) is Element of bool X

((Ser (C * Q)) . y) + (C . F9) is ext-real Element of ExtREAL

C . (F9 \/ (QQ . y)) is ext-real Element of ExtREAL

Ser R is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

y is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

(Ser (C * Q)) . y is ext-real Element of ExtREAL

(Ser R) . y is ext-real Element of ExtREAL

k is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

(Ser R) . k is ext-real Element of ExtREAL

k + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

(Ser R) . (k + 1) is ext-real Element of ExtREAL

R . (k + 1) is ext-real Element of ExtREAL

((Ser R) . k) + (R . (k + 1)) is ext-real Element of ExtREAL

((Ser R) . k) + 0. is ext-real Element of ExtREAL

(Ser R) . 0 is ext-real Element of ExtREAL

R . 0 is ext-real Element of ExtREAL

(Ser R) . 0 is ext-real Element of ExtREAL

R . 0 is ext-real Element of ExtREAL

SUM (C * Q) is ext-real Element of ExtREAL

k is V15() V16() V17() V21() V22() real ext-real non negative V59() V60() V61() V62() V63() V64() Element of NAT

R . k is ext-real Element of ExtREAL

SUM R is ext-real Element of ExtREAL

(Ser R) . 1 is ext-real Element of ExtREAL

0 + 1 is non empty V15() V16() V17() V21() V22() real ext-real positive non negative V59() V60() V61() V62() V63() V64() Element of NAT

R . (0 + 1) is ext-real Element of ExtREAL

((Ser R) . 0) + (R . (0 + 1)) is ext-real Element of ExtREAL

((Ser R) . 0) + 0. is ext-real Element of ExtREAL

+infty is non empty non real ext-real positive non negative Element of ExtREAL

A is set

X \ A is Element of bool X

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

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

X is set

bool X is non empty set

bool (bool X) is non empty set

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

A is non empty V47() N_Sub_fam of C

union A is set

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

[:(X,C),ExtREAL:] is non empty ext-real-valued set

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

A is set

C . A is ext-real Element of ExtREAL

A is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

B is Element of bool X

A . B is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

A is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

A is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

B is Element of bool X

A . B is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

A is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

B is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

B is set

A . B is ext-real Element of ExtREAL

B . B is ext-real Element of ExtREAL

F9 is Element of bool X

A . F9 is ext-real Element of ExtREAL

C . F9 is ext-real Element of ExtREAL

B . F9 is ext-real Element of ExtREAL

dom B is Element of bool (X,C)

bool (X,C) is non empty set

dom A is Element of bool (X,C)

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

(X,C) is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

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

[:(X,C),ExtREAL:] is non empty ext-real-valued set

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

A is Element of (X,C)

B is Element of bool X

(X,C) . B is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

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

(X,C) . {} is ext-real Element of ExtREAL

C . {} is ext-real Element of ExtREAL

A is Element of (X,C)

B is Element of (X,C)

F9 is Element of bool X

(X,C) . F9 is ext-real Element of ExtREAL

C . F9 is ext-real Element of ExtREAL

B is Element of bool X

B \/ F9 is Element of bool X

C . (B \/ F9) is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C . B) + (C . F9) is ext-real Element of ExtREAL

(X,C) . B is ext-real Element of ExtREAL

A \/ B is Element of (X,C)

(X,C) . (A \/ B) is ext-real Element of ExtREAL

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

(X,C) . B is ext-real Element of ExtREAL

((X,C) . A) + ((X,C) . B) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

(X,C) is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

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

[:(X,C),ExtREAL:] is non empty ext-real-valued set

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

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

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

A is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued zeroed nonnegative V90(X,(X,C)) Element of bool [:(X,C),ExtREAL:]

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

rng B is non empty V47() N_Sub_fam of (X,C)

(X,(X,C),(rng B)) is Element of (X,C)

A . (X,(X,C),(rng B)) is ext-real Element of ExtREAL

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

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

B is Element of bool X

C * B is V1() V4( NAT ) V5( ExtREAL ) Function-like ext-real-valued Element of bool [:NAT,ExtREAL:]

F9 is set

(A * B) . F9 is ext-real Element of ExtREAL

(C * B) . F9 is ext-real Element of ExtREAL

B . F9 is set

A . (B . F9) is ext-real Element of ExtREAL

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

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

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

C * a is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

(C * a) . F9 is ext-real Element of ExtREAL

a . F9 is set

C . (a . F9) is ext-real Element of ExtREAL

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

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

A . B is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

a is ext-real Element of ExtREAL

b is ext-real Element of ExtREAL

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

C * F9 is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

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

C * F is V1() V4( NAT ) V5( ExtREAL ) Function-like non empty V14( NAT ) V30( NAT , ExtREAL ) ext-real-valued Element of bool [:NAT,ExtREAL:]

SUM (C * F) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

(X,C) is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued Element of bool [:(X,C),ExtREAL:]

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

[:(X,C),ExtREAL:] is non empty ext-real-valued set

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

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

A is Element of bool X

C . A is ext-real Element of ExtREAL

B is Element of bool X

B is Element of bool X

X \ A is Element of bool X

B \/ B is Element of bool X

C . B is ext-real Element of ExtREAL

C . (B \/ B) is ext-real Element of ExtREAL

C . B is ext-real Element of ExtREAL

(C . B) + (C . B) is ext-real Element of ExtREAL

X is set

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

bool X is non empty set

bool (bool X) is non empty set

C is V1() V4( bool X) V5( ExtREAL ) Function-like non empty V14( bool X) V30( bool X, ExtREAL ) ext-real-valued (X)

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

(X,C) is V1() V4((X,C)) V5( ExtREAL ) Function-like non empty V14((X,C)) V30((X,C), ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of bool [:(X,C),ExtREAL:]

[:(X,C),ExtREAL:] is non empty ext-real-valued set

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

A is Element of bool X

B is set

(X,C) . B is ext-real Element of ExtREAL

C . A is ext-real Element of ExtREAL

B is Element of bool X

C . B is ext-real Element of ExtREAL