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