REAL is non empty V27() V156() V157() V158() V162() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V156() V157() V158() V159() V160() V161() V162() Element of bool REAL
bool REAL is non empty set
ExtREAL is non empty V157() set
[:NAT,ExtREAL:] is non empty V164() set
bool [:NAT,ExtREAL:] is non empty set
bool ExtREAL is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V156() V157() V158() V159() V160() V161() V162() set
bool omega is non empty set
bool NAT is non empty set
COMPLEX is non empty V27() V156() V162() set
[:NAT,REAL:] is non empty V163() V164() V165() set
bool [:NAT,REAL:] is non empty set
bool (bool REAL) is non empty set
RAT is non empty V27() V156() V157() V158() V159() V162() set
INT is non empty V27() V156() V157() V158() V159() V160() V162() set
{} is set
the empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V38() real V156() V157() V158() V159() V160() V161() V162() set is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural ext-real non positive non negative V38() real V156() V157() V158() V159() V160() V161() V162() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
{{},1} is set
[:NAT,COMPLEX:] is non empty V163() set
bool [:NAT,COMPLEX:] is non empty set
K657() is non empty set
[:K657(),K657():] is non empty set
[:[:K657(),K657():],K657():] is non empty set
bool [:[:K657(),K657():],K657():] is non empty set
[:REAL,K657():] is non empty set
[:[:REAL,K657():],K657():] is non empty set
bool [:[:REAL,K657():],K657():] is non empty set
K663() is RLSStruct
the carrier of K663() is set
bool the carrier of K663() is non empty set
K667() is Element of bool the carrier of K663()
[:K667(),K667():] is set
[:[:K667(),K667():],REAL:] is V163() V164() V165() set
bool [:[:K667(),K667():],REAL:] is non empty set
the_set_of_l1RealSequences is Element of bool the carrier of K663()
[:the_set_of_l1RealSequences,REAL:] is V163() V164() V165() set
bool [:the_set_of_l1RealSequences,REAL:] is non empty set
bool RAT is non empty set
[:COMPLEX,COMPLEX:] is non empty V163() set
bool [:COMPLEX,COMPLEX:] is non empty set
[:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty V163() set
bool [:[:COMPLEX,COMPLEX:],COMPLEX:] is non empty set
[:REAL,REAL:] is non empty V163() V164() V165() set
bool [:REAL,REAL:] is non empty set
[:[:REAL,REAL:],REAL:] is non empty V163() V164() V165() set
bool [:[:REAL,REAL:],REAL:] is non empty set
[:RAT,RAT:] is V5( RAT ) non empty V163() V164() V165() set
bool [:RAT,RAT:] is non empty set
[:[:RAT,RAT:],RAT:] is V5( RAT ) non empty V163() V164() V165() set
bool [:[:RAT,RAT:],RAT:] is non empty set
[:INT,INT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() set
bool [:INT,INT:] is non empty set
[:[:INT,INT:],INT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() set
bool [:[:INT,INT:],INT:] is non empty set
[:NAT,NAT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() V166() set
[:[:NAT,NAT:],NAT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() V166() set
bool [:[:NAT,NAT:],NAT:] is non empty set
0 is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
|.0.| is ext-real V38() real V194() Element of REAL
bool [:NAT,NAT:] is non empty set
- 1 is non empty ext-real non positive negative V38() real Element of REAL
0. is ext-real Element of ExtREAL
K626() is non empty ext-real positive non negative non real Element of ExtREAL
K627() is non empty ext-real non positive negative non real Element of ExtREAL
+infty is non empty ext-real positive non negative non real set
-infty is non empty ext-real non positive negative non real set
X is non empty ext-real positive non negative V38() real set
1 / X is non empty ext-real positive non negative V38() real Element of REAL
X " is non empty ext-real positive non negative V38() real set
1 * (X ") is non empty ext-real positive non negative V38() real set
S is non empty ext-real positive non negative V38() real set
1 / S is non empty ext-real positive non negative V38() real Element of REAL
S " is non empty ext-real positive non negative V38() real set
1 * (S ") is non empty ext-real positive non negative V38() real set
(1 / X) + (1 / S) is non empty ext-real positive non negative V38() real Element of REAL
1 - (1 / X) is ext-real V38() real Element of REAL
- (1 / X) is non empty ext-real non positive negative V38() real set
1 + (- (1 / X)) is ext-real V38() real set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,ExtREAL:] is non empty V164() set
bool [:X,ExtREAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is Element of S
g is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
dom g is Element of bool X
Integral (M,g) is ext-real Element of ExtREAL
max+ g is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ g)) is ext-real Element of ExtREAL
max- g is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max- g)) is ext-real Element of ExtREAL
(integral+ (M,(max+ g))) - (integral+ (M,(max- g))) is ext-real Element of ExtREAL
dom (max- g) is Element of bool X
dom (max+ g) is Element of bool X
a is Element of X
(max+ g) . a is ext-real set
Integral (M,(max+ g)) is ext-real Element of ExtREAL
max+ (max+ g) is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (max+ g))) is ext-real Element of ExtREAL
max- (max+ g) is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (max+ g))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (max+ g)))) - (integral+ (M,(max- (max+ g)))) is ext-real Element of ExtREAL
a is Element of X
(max+ g) . a is ext-real set
g . a is ext-real set
max ((g . a),0) is ext-real set
a is Element of X
(max- g) . a is ext-real set
Integral (M,(max- g)) is ext-real Element of ExtREAL
max+ (max- g) is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (max- g))) is ext-real Element of ExtREAL
max- (max- g) is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (max- g))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (max- g)))) - (integral+ (M,(max- (max- g)))) is ext-real Element of ExtREAL
a is Element of X
(max- g) . a is ext-real set
(max+ g) . a is ext-real set
g . a is ext-real set
X is ext-real V38() real set
M is ext-real V38() real Element of REAL
X is ext-real V38() real Element of REAL
S is ext-real V38() real Element of REAL
S to_power M is ext-real V38() real Element of REAL
X to_power M is ext-real V38() real Element of REAL
X is ext-real V38() real Element of REAL
S is ext-real V38() real Element of REAL
X to_power S is ext-real V38() real Element of REAL
X is ext-real V38() real Element of REAL
S is ext-real V38() real Element of REAL
X * S is ext-real V38() real Element of REAL
M is ext-real V38() real Element of REAL
(X * S) to_power M is ext-real V38() real Element of REAL
X to_power M is ext-real V38() real Element of REAL
S to_power M is ext-real V38() real Element of REAL
(X to_power M) * (S to_power M) is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is ext-real V38() real Element of REAL
M is ext-real V38() real Element of REAL
S * M is ext-real V38() real Element of REAL
x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x to_power S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(x to_power S) to_power M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x to_power (S * M) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom (x to_power S) is Element of bool X
bool X is non empty set
dom x is Element of bool X
dom ((x to_power S) to_power M) is Element of bool X
dom (x to_power (S * M)) is Element of bool X
g is set
((x to_power S) to_power M) . g is ext-real V38() real Element of REAL
(x to_power (S * M)) . g is ext-real V38() real Element of REAL
(x to_power S) . g is ext-real V38() real Element of REAL
((x to_power S) . g) to_power M is ext-real V38() real Element of REAL
x . g is ext-real V38() real Element of REAL
(x . g) to_power S is ext-real V38() real Element of REAL
((x . g) to_power S) to_power M is ext-real V38() real Element of REAL
(x . g) to_power (S * M) is ext-real V38() real Element of REAL
0 to_power M is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is ext-real V38() real Element of REAL
M is ext-real V38() real Element of REAL
S + M is ext-real V38() real Element of REAL
x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x to_power S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x to_power M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(x to_power S) (#) (x to_power M) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x to_power (S + M) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom (x to_power S) is Element of bool X
bool X is non empty set
dom x is Element of bool X
dom (x to_power M) is Element of bool X
dom ((x to_power S) (#) (x to_power M)) is Element of bool X
(dom (x to_power S)) /\ (dom (x to_power M)) is Element of bool X
dom (x to_power (S + M)) is Element of bool X
g is set
((x to_power S) (#) (x to_power M)) . g is ext-real V38() real Element of REAL
(x to_power (S + M)) . g is ext-real V38() real Element of REAL
(x to_power S) . g is ext-real V38() real Element of REAL
x . g is ext-real V38() real Element of REAL
(x . g) to_power S is ext-real V38() real Element of REAL
(x to_power M) . g is ext-real V38() real Element of REAL
(x . g) to_power M is ext-real V38() real Element of REAL
((x . g) to_power S) * ((x . g) to_power M) is ext-real V38() real Element of REAL
(x . g) to_power (S + M) is ext-real V38() real Element of REAL
0 to_power M is ext-real V38() real Element of REAL
0 * (0 to_power M) is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
S to_power 1 is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom (S to_power 1) is Element of bool X
bool X is non empty set
dom S is Element of bool X
M is set
(S to_power 1) . M is ext-real V38() real Element of REAL
S . M is ext-real V38() real Element of REAL
(S . M) to_power 1 is ext-real V38() real Element of REAL
X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
S is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
M is non empty ext-real positive non negative V38() real Element of REAL
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
X . x is ext-real V38() real Element of REAL
S . x is ext-real V38() real Element of REAL
(S . x) to_power M is ext-real V38() real Element of REAL
1 / M is non empty ext-real positive non negative V38() real Element of REAL
M " is non empty ext-real positive non negative V38() real set
1 * (M ") is non empty ext-real positive non negative V38() real set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
S . x is ext-real V38() real Element of REAL
X . x is ext-real V38() real Element of REAL
(X . x) to_power (1 / M) is ext-real V38() real Element of REAL
(S . x) to_power M is ext-real V38() real Element of REAL
((S . x) to_power M) to_power (1 / M) is ext-real V38() real Element of REAL
M * (1 / M) is non empty ext-real positive non negative V38() real Element of REAL
(S . x) to_power (M * (1 / M)) is ext-real V38() real Element of REAL
(S . x) to_power 1 is ext-real V38() real Element of REAL
X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
Partial_Sums X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
abs X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
Partial_Sums (abs X) is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
S is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
(Partial_Sums X) . S is ext-real V38() real Element of REAL
(Partial_Sums X) . M is ext-real V38() real Element of REAL
((Partial_Sums X) . S) - ((Partial_Sums X) . M) is ext-real V38() real Element of REAL
- ((Partial_Sums X) . M) is ext-real V38() real set
((Partial_Sums X) . S) + (- ((Partial_Sums X) . M)) is ext-real V38() real set
abs (((Partial_Sums X) . S) - ((Partial_Sums X) . M)) is ext-real V38() real Element of REAL
(Partial_Sums (abs X)) . S is ext-real V38() real Element of REAL
(Partial_Sums (abs X)) . M is ext-real V38() real Element of REAL
((Partial_Sums (abs X)) . S) - ((Partial_Sums (abs X)) . M) is ext-real V38() real Element of REAL
- ((Partial_Sums (abs X)) . M) is ext-real V38() real set
((Partial_Sums (abs X)) . S) + (- ((Partial_Sums (abs X)) . M)) is ext-real V38() real set
x is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
(abs X) . x is ext-real V38() real Element of REAL
X . x is ext-real V38() real Element of REAL
abs (X . x) is ext-real V38() real Element of REAL
abs (((Partial_Sums (abs X)) . S) - ((Partial_Sums (abs X)) . M)) is ext-real V38() real Element of REAL
(((Partial_Sums (abs X)) . S) - ((Partial_Sums (abs X)) . M)) + ((Partial_Sums (abs X)) . M) is ext-real V38() real Element of REAL
X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
S is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
lim X is ext-real V38() real Element of REAL
lim S is ext-real V38() real Element of REAL
M is non empty ext-real positive non negative V38() real Element of REAL
g is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
a is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real set
a . b is ext-real V38() real Element of REAL
a - X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
- X is V1() V4( NAT ) Function-like total V163() V164() V165() set
- 1 is non empty ext-real non positive negative V38() real set
(- 1) (#) X is V1() V4( NAT ) Function-like total V163() V164() V165() set
a + (- X) is V1() V4( NAT ) Function-like total V163() V164() V165() set
dom a is V156() V157() V158() V159() V160() V161() Element of bool NAT
dom X is V156() V157() V158() V159() V160() V161() Element of bool NAT
dom (a - X) is V156() V157() V158() V159() V160() V161() Element of bool NAT
dom g is V156() V157() V158() V159() V160() V161() Element of bool NAT
abs (a - X) is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
dom (abs (a - X)) is V156() V157() V158() V159() V160() V161() Element of bool NAT
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
(abs (a - X)) . b is ext-real V38() real Element of REAL
g . b is ext-real V38() real Element of REAL
X . b is ext-real V38() real Element of REAL
(lim X) - (X . b) is ext-real V38() real Element of REAL
- (X . b) is ext-real V38() real set
(lim X) + (- (X . b)) is ext-real V38() real set
|.((lim X) - (X . b)).| is ext-real V38() real Element of REAL
a . b is ext-real V38() real Element of REAL
(a . b) - (X . b) is ext-real V38() real Element of REAL
(a . b) + (- (X . b)) is ext-real V38() real set
|.((a . b) - (X . b)).| is ext-real V38() real Element of REAL
(a - X) . b is ext-real V38() real Element of REAL
abs ((a - X) . b) is ext-real V38() real Element of REAL
lim (a - X) is ext-real V38() real Element of REAL
a . 0 is ext-real V38() real Element of REAL
(a . 0) - (lim X) is ext-real V38() real Element of REAL
- (lim X) is ext-real V38() real set
(a . 0) + (- (lim X)) is ext-real V38() real set
(lim X) - (lim X) is ext-real V38() real Element of REAL
(lim X) + (- (lim X)) is ext-real V38() real set
lim g is ext-real V38() real Element of REAL
b is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
S . b is ext-real V38() real Element of REAL
g . b is ext-real V38() real Element of REAL
(g . b) to_power M is ext-real V38() real Element of REAL
X . b is ext-real V38() real Element of REAL
(lim X) - (X . b) is ext-real V38() real Element of REAL
- (X . b) is ext-real V38() real set
(lim X) + (- (X . b)) is ext-real V38() real set
|.((lim X) - (X . b)).| is ext-real V38() real Element of REAL
(lim g) to_power M is ext-real V38() real Element of REAL
X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
Partial_Sums X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
S is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
(Partial_Sums X) . S is ext-real V38() real Element of REAL
abs ((Partial_Sums X) . S) is ext-real V38() real Element of REAL
abs X is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
Partial_Sums (abs X) is V1() V4( NAT ) V5( REAL ) Function-like non empty total V41( NAT , REAL ) V163() V164() V165() Element of bool [:NAT,REAL:]
(Partial_Sums (abs X)) . S is ext-real V38() real Element of REAL
X is non empty ext-real positive non negative V38() real Element of REAL
S is non empty set
S --> 0 is V1() V4(S) V5( REAL ) V5( RAT ) V5( INT ) Function-like V163() V164() V165() V166() Element of bool [:S,REAL:]
[:S,REAL:] is non empty V163() V164() V165() set
bool [:S,REAL:] is non empty set
(S --> 0) to_power X is V1() V4(S) V5( REAL ) Function-like V163() V164() V165() Element of bool [:S,REAL:]
dom ((S --> 0) to_power X) is Element of bool S
bool S is non empty set
dom (S --> 0) is Element of bool S
M is Element of S
((S --> 0) to_power X) . M is ext-real V38() real Element of REAL
(S --> 0) . M is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
((S --> 0) . M) to_power X is ext-real V38() real Element of REAL
0 to_power X is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M is set
S | M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs (S | M) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(abs S) | M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom (abs (S | M)) is Element of bool X
bool X is non empty set
dom (S | M) is Element of bool X
dom S is Element of bool X
(dom S) /\ M is Element of bool X
dom (abs S) is Element of bool X
(dom (abs S)) /\ M is Element of bool X
dom ((abs S) | M) is Element of bool X
x is Element of X
(abs (S | M)) . x is ext-real V38() real Element of REAL
((abs S) | M) . x is ext-real V38() real Element of REAL
(S | M) . x is ext-real V38() real Element of REAL
abs ((S | M) . x) is ext-real V38() real Element of REAL
S . x is ext-real V38() real Element of REAL
abs (S . x) is ext-real V38() real Element of REAL
(abs S) . x is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M is set
dom (abs S) is Element of bool X
bool X is non empty set
(abs S) . M is ext-real V38() real Element of REAL
S . M is ext-real V38() real Element of REAL
abs (S . M) is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
dom S is Element of bool X
bool X is non empty set
dom (abs S) is Element of bool X
M is Element of X
S . M is ext-real V38() real Element of REAL
(abs S) . M is ext-real V38() real Element of REAL
abs (S . M) is ext-real V38() real Element of REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom x is Element of bool X
Integral (M,x) is ext-real Element of ExtREAL
R_EAL x is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
[:X,ExtREAL:] is non empty V164() set
bool [:X,ExtREAL:] is non empty set
Integral (M,(R_EAL x)) is ext-real Element of ExtREAL
max+ (R_EAL x) is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max+ (R_EAL x))) is ext-real Element of ExtREAL
max- (R_EAL x) is V1() V4(X) V5( ExtREAL ) Function-like V164() Element of bool [:X,ExtREAL:]
integral+ (M,(max- (R_EAL x))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (R_EAL x)))) - (integral+ (M,(max- (R_EAL x)))) is ext-real Element of ExtREAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is non empty ext-real positive non negative V38() real Element of REAL
{ b1 where b1 is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:] : ex b2 being Element of S st
( M . (b2 `) = 0 & dom b1 = b2 & b1 is_measurable_on b2 & (abs b1) to_power x is_integrable_on M ) } is set
RLSp_PFunct X is non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
PFuncs (X,REAL) is functional non empty PartFunc-set of X, REAL
RealPFuncZero X is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of PFuncs (X,REAL)
K517(NAT,X,0) is V1() V4(X) V5( NAT ) V5( RAT ) V5( INT ) Function-like non empty total V41(X, NAT ) V163() V164() V165() V166() Element of bool [:X,NAT:]
[:X,NAT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() V166() set
bool [:X,NAT:] is non empty set
addpfunc X is V1() V4([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set
[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
multrealpfunc X is V1() V4([:REAL,(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:REAL,(PFuncs (X,REAL)):] is non empty set
[:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
RLSStruct(# (PFuncs (X,REAL)),(RealPFuncZero X),(addpfunc X),(multrealpfunc X) #) is non empty strict RLSStruct
the carrier of (RLSp_PFunct X) is non empty set
bool the carrier of (RLSp_PFunct X) is non empty set
a is set
b is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
ND is Element of S
ND ` is Element of bool X
X \ ND is set
M . (ND `) is ext-real set
dom b is Element of bool X
abs b is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs b) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
X --> 0 is V1() V4(X) V5( REAL ) V5( RAT ) V5( INT ) Function-like V163() V164() V165() V166() Element of bool [:X,REAL:]
a is V1() V4(X) V5( REAL ) Function-like non empty total V41(X, REAL ) V163() V164() V165() Element of bool [:X,REAL:]
abs a is V1() V4(X) V5( REAL ) Function-like non empty total V41(X, REAL ) V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs a) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
dom a is Element of bool X
Ef is set
a . Ef is ext-real V38() real Element of REAL
b is Element of S
b ` is Element of bool X
X \ b is set
M . (b `) is ext-real set
dom (X --> 0) is Element of bool X
Ef is set
(X --> 0) . Ef is epsilon-transitive epsilon-connected ordinal natural ext-real non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
dom ((abs a) to_power x) is Element of bool X
Ef is Element of X
((abs a) to_power x) . Ef is ext-real V38() real Element of REAL
2 is non empty epsilon-transitive epsilon-connected ordinal natural ext-real positive non negative V38() real V104() V156() V157() V158() V159() V160() V161() V194() Element of NAT
M is ext-real V38() real Element of REAL
X is ext-real V38() real Element of REAL
S is ext-real V38() real Element of REAL
X + S is ext-real V38() real Element of REAL
abs (X + S) is ext-real V38() real Element of REAL
(abs (X + S)) to_power M is ext-real V38() real Element of REAL
abs X is ext-real V38() real Element of REAL
abs S is ext-real V38() real Element of REAL
(abs X) + (abs S) is ext-real V38() real Element of REAL
((abs X) + (abs S)) to_power M is ext-real V38() real Element of REAL
max ((abs X),(abs S)) is ext-real V38() real set
2 * (max ((abs X),(abs S))) is ext-real V38() real Element of REAL
(2 * (max ((abs X),(abs S)))) to_power M is ext-real V38() real Element of REAL
(max ((abs X),(abs S))) + (max ((abs X),(abs S))) is ext-real V38() real set
X is ext-real V38() real Element of REAL
S is ext-real V38() real Element of REAL
M is ext-real V38() real Element of REAL
max (X,S) is ext-real V38() real set
(max (X,S)) to_power M is ext-real V38() real set
X to_power M is ext-real V38() real Element of REAL
S to_power M is ext-real V38() real Element of REAL
(X to_power M) + (S to_power M) is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
x is ext-real V38() real Element of REAL
(abs S) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M is ext-real V38() real Element of REAL
abs M is ext-real V38() real Element of REAL
(abs M) to_power x is ext-real V38() real Element of REAL
((abs M) to_power x) (#) ((abs S) to_power x) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M (#) S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs (M (#) S) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs (M (#) S)) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom (((abs M) to_power x) (#) ((abs S) to_power x)) is Element of bool X
bool X is non empty set
dom ((abs S) to_power x) is Element of bool X
dom (M (#) S) is Element of bool X
dom S is Element of bool X
dom (abs S) is Element of bool X
dom (abs (M (#) S)) is Element of bool X
dom ((abs (M (#) S)) to_power x) is Element of bool X
g is Element of X
(((abs M) to_power x) (#) ((abs S) to_power x)) . g is ext-real V38() real Element of REAL
((abs (M (#) S)) to_power x) . g is ext-real V38() real Element of REAL
S . g is ext-real V38() real Element of REAL
abs (S . g) is ext-real V38() real Element of REAL
((abs S) to_power x) . g is ext-real V38() real Element of REAL
((abs M) to_power x) * (((abs S) to_power x) . g) is ext-real V38() real Element of REAL
(abs S) . g is ext-real V38() real Element of REAL
((abs S) . g) to_power x is ext-real V38() real Element of REAL
((abs M) to_power x) * (((abs S) . g) to_power x) is ext-real V38() real Element of REAL
(abs (S . g)) to_power x is ext-real V38() real Element of REAL
((abs M) to_power x) * ((abs (S . g)) to_power x) is ext-real V38() real Element of REAL
(abs M) * (abs (S . g)) is ext-real V38() real Element of REAL
((abs M) * (abs (S . g))) to_power x is ext-real V38() real Element of REAL
M * (S . g) is ext-real V38() real Element of REAL
abs (M * (S . g)) is ext-real V38() real Element of REAL
(abs (M * (S . g))) to_power x is ext-real V38() real Element of REAL
(M (#) S) . g is ext-real V38() real Element of REAL
abs ((M (#) S) . g) is ext-real V38() real Element of REAL
(abs ((M (#) S) . g)) to_power x is ext-real V38() real Element of REAL
(abs (M (#) S)) . g is ext-real V38() real Element of REAL
((abs (M (#) S)) . g) to_power x is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
M is ext-real V38() real Element of REAL
x is ext-real V38() real Element of REAL
(abs S) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M to_power x is ext-real V38() real Element of REAL
(M to_power x) (#) ((abs S) to_power x) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M (#) (abs S) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(M (#) (abs S)) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs M is ext-real V38() real Element of REAL
M (#) S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs (M (#) S) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs (M (#) S)) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
M is ext-real V38() real set
S to_power M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x is set
S | x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(S | x) to_power M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(S to_power M) | x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom ((S | x) to_power M) is Element of bool X
bool X is non empty set
dom (S | x) is Element of bool X
dom S is Element of bool X
(dom S) /\ x is Element of bool X
dom (S to_power M) is Element of bool X
(dom (S to_power M)) /\ x is Element of bool X
dom ((S to_power M) | x) is Element of bool X
g is Element of X
((S | x) to_power M) . g is ext-real V38() real Element of REAL
(S | x) . g is ext-real V38() real Element of REAL
((S | x) . g) to_power M is ext-real V38() real set
S . g is ext-real V38() real Element of REAL
(S . g) to_power M is ext-real V38() real set
(S to_power M) . g is ext-real V38() real Element of REAL
((S to_power M) | x) . g is ext-real V38() real Element of REAL
M is ext-real V38() real Element of REAL
X is ext-real V38() real Element of REAL
S is ext-real V38() real Element of REAL
X + S is ext-real V38() real Element of REAL
abs (X + S) is ext-real V38() real Element of REAL
(abs (X + S)) to_power M is ext-real V38() real Element of REAL
2 to_power M is ext-real V38() real Element of REAL
abs X is ext-real V38() real Element of REAL
(abs X) to_power M is ext-real V38() real Element of REAL
abs S is ext-real V38() real Element of REAL
(abs S) to_power M is ext-real V38() real Element of REAL
((abs X) to_power M) + ((abs S) to_power M) is ext-real V38() real Element of REAL
(2 to_power M) * (((abs X) to_power M) + ((abs S) to_power M)) is ext-real V38() real Element of REAL
max ((abs X),(abs S)) is ext-real V38() real set
2 * (max ((abs X),(abs S))) is ext-real V38() real Element of REAL
(2 * (max ((abs X),(abs S)))) to_power M is ext-real V38() real Element of REAL
(max ((abs X),(abs S))) to_power M is ext-real V38() real set
(2 to_power M) * ((max ((abs X),(abs S))) to_power M) is ext-real V38() real Element of REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is non empty ext-real positive non negative V38() real Element of REAL
(X,S,M,x) is non empty Element of bool the carrier of (RLSp_PFunct X)
RLSp_PFunct X is non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
PFuncs (X,REAL) is functional non empty PartFunc-set of X, REAL
RealPFuncZero X is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of PFuncs (X,REAL)
K517(NAT,X,0) is V1() V4(X) V5( NAT ) V5( RAT ) V5( INT ) Function-like non empty total V41(X, NAT ) V163() V164() V165() V166() Element of bool [:X,NAT:]
[:X,NAT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() V166() set
bool [:X,NAT:] is non empty set
addpfunc X is V1() V4([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set
[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
multrealpfunc X is V1() V4([:REAL,(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:REAL,(PFuncs (X,REAL)):] is non empty set
[:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
RLSStruct(# (PFuncs (X,REAL)),(RealPFuncZero X),(addpfunc X),(multrealpfunc X) #) is non empty strict RLSStruct
the carrier of (RLSp_PFunct X) is non empty set
bool the carrier of (RLSp_PFunct X) is non empty set
{ b1 where b1 is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:] : ex b2 being Element of S st
( M . (b2 `) = 0 & dom b1 = b2 & b1 is_measurable_on b2 & (abs b1) to_power x is_integrable_on M ) } is set
g is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
a is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs g is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs g) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
abs a is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs a) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
((abs g) to_power x) + ((abs a) to_power x) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
b is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
ND is Element of S
ND ` is Element of bool X
X \ ND is set
M . (ND `) is ext-real set
dom b is Element of bool X
abs b is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs b) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
Ef is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
E is Element of S
E ` is Element of bool X
X \ E is set
M . (E `) is ext-real set
dom Ef is Element of bool X
abs Ef is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs Ef) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
X --> 0 is V1() V4(X) V5( REAL ) V5( RAT ) V5( INT ) Function-like V163() V164() V165() V166() Element of bool [:X,REAL:]
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is non empty ext-real positive non negative V38() real Element of REAL
(X,S,M,x) is non empty Element of bool the carrier of (RLSp_PFunct X)
RLSp_PFunct X is non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
PFuncs (X,REAL) is functional non empty PartFunc-set of X, REAL
RealPFuncZero X is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of PFuncs (X,REAL)
K517(NAT,X,0) is V1() V4(X) V5( NAT ) V5( RAT ) V5( INT ) Function-like non empty total V41(X, NAT ) V163() V164() V165() V166() Element of bool [:X,NAT:]
[:X,NAT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() V166() set
bool [:X,NAT:] is non empty set
addpfunc X is V1() V4([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set
[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
multrealpfunc X is V1() V4([:REAL,(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:REAL,(PFuncs (X,REAL)):] is non empty set
[:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
RLSStruct(# (PFuncs (X,REAL)),(RealPFuncZero X),(addpfunc X),(multrealpfunc X) #) is non empty strict RLSStruct
the carrier of (RLSp_PFunct X) is non empty set
bool the carrier of (RLSp_PFunct X) is non empty set
{ b1 where b1 is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:] : ex b2 being Element of S st
( M . (b2 `) = 0 & dom b1 = b2 & b1 is_measurable_on b2 & (abs b1) to_power x is_integrable_on M ) } is set
a is Element of S
a ` is Element of bool X
X \ a is set
M . (a `) is ext-real set
g is V1() V4(X) V5( REAL ) Function-like non empty total V41(X, REAL ) V163() V164() V165() Element of bool [:X,REAL:]
dom g is Element of bool X
b is Element of X
g . b is ext-real V38() real Element of REAL
b is set
g . b is ext-real V38() real Element of REAL
abs g is V1() V4(X) V5( REAL ) Function-like non empty total V41(X, REAL ) V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs g) to_power x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
b is set
g . b is ext-real V38() real Element of REAL
X is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is ext-real V38() real Element of REAL
2 to_power S is ext-real V38() real Element of REAL
M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom M is Element of bool X
bool X is non empty set
x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom x is Element of bool X
(dom M) /\ (dom x) is Element of bool X
M + x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs (M + x) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs (M + x)) to_power S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs M is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs M) to_power S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
abs x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs x) to_power S is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
((abs M) to_power S) + ((abs x) to_power S) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(2 to_power S) (#) (((abs M) to_power S) + ((abs x) to_power S)) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
g is Element of X
((abs (M + x)) to_power S) . g is ext-real V38() real Element of REAL
((2 to_power S) (#) (((abs M) to_power S) + ((abs x) to_power S))) . g is ext-real V38() real Element of REAL
dom (M + x) is Element of bool X
dom (abs (M + x)) is Element of bool X
dom ((abs (M + x)) to_power S) is Element of bool X
(abs (M + x)) . g is ext-real V38() real Element of REAL
((abs (M + x)) . g) to_power S is ext-real V38() real Element of REAL
(M + x) . g is ext-real V38() real Element of REAL
abs ((M + x) . g) is ext-real V38() real Element of REAL
(abs ((M + x) . g)) to_power S is ext-real V38() real Element of REAL
M . g is ext-real V38() real Element of REAL
x . g is ext-real V38() real Element of REAL
(M . g) + (x . g) is ext-real V38() real Element of REAL
abs ((M . g) + (x . g)) is ext-real V38() real Element of REAL
(abs ((M . g) + (x . g))) to_power S is ext-real V38() real Element of REAL
dom (abs M) is Element of bool X
dom (abs x) is Element of bool X
dom ((abs M) to_power S) is Element of bool X
dom ((abs x) to_power S) is Element of bool X
abs (M . g) is ext-real V38() real Element of REAL
(abs (M . g)) to_power S is ext-real V38() real Element of REAL
(abs M) . g is ext-real V38() real Element of REAL
((abs M) . g) to_power S is ext-real V38() real Element of REAL
abs (x . g) is ext-real V38() real Element of REAL
(abs (x . g)) to_power S is ext-real V38() real Element of REAL
(abs x) . g is ext-real V38() real Element of REAL
((abs x) . g) to_power S is ext-real V38() real Element of REAL
((abs M) to_power S) . g is ext-real V38() real Element of REAL
((abs x) to_power S) . g is ext-real V38() real Element of REAL
dom (((abs M) to_power S) + ((abs x) to_power S)) is Element of bool X
(dom ((abs M) to_power S)) /\ (dom ((abs x) to_power S)) is Element of bool X
((abs (M . g)) to_power S) + ((abs (x . g)) to_power S) is ext-real V38() real Element of REAL
(2 to_power S) * (((abs (M . g)) to_power S) + ((abs (x . g)) to_power S)) is ext-real V38() real Element of REAL
(((abs M) to_power S) + ((abs x) to_power S)) . g is ext-real V38() real Element of REAL
(2 to_power S) * ((((abs M) to_power S) + ((abs x) to_power S)) . g) is ext-real V38() real Element of REAL
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
g is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
x + g is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
a is non empty ext-real positive non negative V38() real Element of REAL
(X,S,M,a) is non empty Element of bool the carrier of (RLSp_PFunct X)
RLSp_PFunct X is non empty strict Abelian add-associative right_zeroed vector-distributive scalar-distributive scalar-associative scalar-unital zeroed RLSStruct
PFuncs (X,REAL) is functional non empty PartFunc-set of X, REAL
RealPFuncZero X is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of PFuncs (X,REAL)
K517(NAT,X,0) is V1() V4(X) V5( NAT ) V5( RAT ) V5( INT ) Function-like non empty total V41(X, NAT ) V163() V164() V165() V166() Element of bool [:X,NAT:]
[:X,NAT:] is V5( RAT ) V5( INT ) non empty V163() V164() V165() V166() set
bool [:X,NAT:] is non empty set
addpfunc X is V1() V4([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:(PFuncs (X,REAL)),(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):] is non empty set
[:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:(PFuncs (X,REAL)),(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
multrealpfunc X is V1() V4([:REAL,(PFuncs (X,REAL)):]) V5( PFuncs (X,REAL)) Function-like non empty total V41([:REAL,(PFuncs (X,REAL)):], PFuncs (X,REAL)) Element of bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):]
[:REAL,(PFuncs (X,REAL)):] is non empty set
[:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
bool [:[:REAL,(PFuncs (X,REAL)):],(PFuncs (X,REAL)):] is non empty set
RLSStruct(# (PFuncs (X,REAL)),(RealPFuncZero X),(addpfunc X),(multrealpfunc X) #) is non empty strict RLSStruct
the carrier of (RLSp_PFunct X) is non empty set
bool the carrier of (RLSp_PFunct X) is non empty set
{ b1 where b1 is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:] : ex b2 being Element of S st
( M . (b2 `) = 0 & dom b1 = b2 & b1 is_measurable_on b2 & (abs b1) to_power a is_integrable_on M ) } is set
ND is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom ND is Element of bool X
abs ND is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs ND) to_power a is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
Ef is Element of S
Ef ` is Element of bool X
X \ Ef is set
M . (Ef `) is ext-real set
Ef is Element of S
Ef ` is Element of bool X
X \ Ef is set
M . (Ef `) is ext-real set
E is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom E is Element of bool X
abs E is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs E) to_power a is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
EE is Element of S
EE ` is Element of bool X
X \ EE is set
M . (EE `) is ext-real set
EE is Element of S
EE ` is Element of bool X
X \ EE is set
M . (EE `) is ext-real set
ND + E is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
dom (ND + E) is Element of bool X
Ef /\ EE is Element of S
abs (ND + E) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
(abs (ND + E)) to_power a is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
((abs ND) to_power a) + ((abs E) to_power a) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
2 to_power a is ext-real V38() real Element of REAL
(2 to_power a) (#) (((abs ND) to_power a) + ((abs E) to_power a)) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
(Ef /\ EE) ` is Element of bool X
X \ (Ef /\ EE) is set
X \ Ef is Element of bool X
X \ EE is Element of bool X
(X \ Ef) \/ (X \ EE) is Element of bool X
(Ef `) \/ (EE `) is Element of bool X
M . ((Ef /\ EE) `) is ext-real set
G is Element of S
G ` is Element of bool X
X \ G is set
M . (G `) is ext-real set
Gp is Element of S
Gp ` is Element of bool X
X \ Gp is set
M . (Gp `) is ext-real set
dom (abs ND) is Element of bool X
dom (abs E) is Element of bool X
dom (abs (ND + E)) is Element of bool X
abs ((abs (ND + E)) to_power a) is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() nonnegative Element of bool [:X,REAL:]
dom ((abs (ND + E)) to_power a) is Element of bool X
dom ((2 to_power a) (#) (((abs ND) to_power a) + ((abs E) to_power a))) is Element of bool X
dom (((abs ND) to_power a) + ((abs E) to_power a)) is Element of bool X
dom ((abs ND) to_power a) is Element of bool X
dom ((abs E) to_power a) is Element of bool X
(dom ((abs ND) to_power a)) /\ (dom ((abs E) to_power a)) is Element of bool X
(dom (abs ND)) /\ (dom ((abs E) to_power a)) is Element of bool X
(dom (abs ND)) /\ (dom (abs E)) is Element of bool X
G is Element of X
(abs ((abs (ND + E)) to_power a)) . G is ext-real V38() real Element of REAL
((2 to_power a) (#) (((abs ND) to_power a) + ((abs E) to_power a))) . G is ext-real V38() real Element of REAL
((abs (ND + E)) to_power a) . G is ext-real V38() real Element of REAL
abs (((abs (ND + E)) to_power a) . G) is ext-real V38() real Element of REAL
G is Element of S
G ` is Element of bool X
X \ G is set
M . (G `) is ext-real set
Gp is Element of S
Gp ` is Element of bool X
X \ Gp is set
M . (Gp `) is ext-real set
X is non empty set
bool X is non empty set
bool (bool X) is non empty set
[:X,REAL:] is non empty V163() V164() V165() set
bool [:X,REAL:] is non empty set
S is non empty compl-closed sigma-multiplicative V152() V153() V154() sigma-additive Element of bool (bool X)
[:S,ExtREAL:] is non empty V164() set
bool [:S,ExtREAL:] is non empty set
M is V1() V4(S) V5( ExtREAL ) Function-like non empty total V41(S, ExtREAL ) V164() V172() nonnegative sigma-additive Element of bool [:S,ExtREAL:]
x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
g is ext-real V38() real Element of REAL
g (#) x is V1() V4(X) V5( REAL ) Function-like V163() V164() V165() Element of bool [:X,REAL:]
a is non empty ext-real positive non negative V38() real Element of REAL
(X,S,M,a) is non empty Element of bool the carrier of (RLSp_PFunct X)
RLSp_PFunct X is non empty strict Abelian