:: MESFUNC7 semantic presentation

REAL is non empty V34() V75() V76() V77() V81() set
NAT is non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() Element of K6(REAL)
K6(REAL) is non empty set
ExtREAL is non empty V76() set
K7(NAT,ExtREAL) is non empty ext-real-valued set
K6(K7(NAT,ExtREAL)) is non empty set
K6(ExtREAL) is non empty set
omega is non empty epsilon-transitive epsilon-connected ordinal V75() V76() V77() V78() V79() V80() V81() set
K6(omega) is non empty set
K6(NAT) is non empty set
K124(NAT) is V33() set
COMPLEX is non empty V34() V75() V81() set
K7(NAT,REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(NAT,REAL)) is non empty set
K6(K6(REAL)) is non empty set
RAT is non empty V34() V75() V76() V77() V78() V81() set
K6(RAT) is non empty set
INT is non empty V34() V75() V76() V77() V78() V79() V81() set
{} is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V21() FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() set
1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
{{},1} is non empty V75() V76() V77() V78() V79() V80() set
K7(COMPLEX,COMPLEX) is non empty complex-valued set
K6(K7(COMPLEX,COMPLEX)) is non empty set
K7(K7(COMPLEX,COMPLEX),COMPLEX) is non empty complex-valued set
K6(K7(K7(COMPLEX,COMPLEX),COMPLEX)) is non empty set
K7(REAL,REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(REAL,REAL)) is non empty set
K7(K7(REAL,REAL),REAL) is non empty complex-valued ext-real-valued real-valued set
K6(K7(K7(REAL,REAL),REAL)) is non empty set
K7(RAT,RAT) is non empty RAT -valued complex-valued ext-real-valued real-valued set
K6(K7(RAT,RAT)) is non empty set
K7(K7(RAT,RAT),RAT) is non empty RAT -valued complex-valued ext-real-valued real-valued set
K6(K7(K7(RAT,RAT),RAT)) is non empty set
K7(INT,INT) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K6(K7(INT,INT)) is non empty set
K7(K7(INT,INT),INT) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K6(K7(K7(INT,INT),INT)) is non empty set
K7(NAT,NAT) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K7(K7(NAT,NAT),NAT) is non empty RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K6(K7(K7(NAT,NAT),NAT)) is non empty set
2 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
3 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
0 is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V21() FinSequence-membered ext-real non positive non negative V51() V75() V76() V77() V78() V79() V80() V81() V84() Element of NAT
0. is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V21() FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() Element of ExtREAL
+infty is non empty non real ext-real positive non negative Element of ExtREAL
-infty is non empty non real ext-real non positive negative Element of ExtREAL
{-infty} is non empty V76() set
{+infty} is non empty V76() set
- 1 is V11() real ext-real non positive Element of REAL
+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} is non empty V76() set
{+infty} is non empty V76() set
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom S is Element of K6(X)
K6(X) is non empty set
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
M - S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
f is ext-real Element of ExtREAL
rng (M - S) is V76() Element of K6(ExtREAL)
dom (M - S) is Element of K6(X)
E is set
(M - S) . E is ext-real Element of ExtREAL
dom M is Element of K6(X)
(dom M) /\ (dom S) is Element of K6(X)
M " {+infty} is Element of K6(X)
S " {+infty} is Element of K6(X)
(M " {+infty}) /\ (S " {+infty}) is Element of K6(X)
M " {-infty} is Element of K6(X)
S " {-infty} is Element of K6(X)
(M " {-infty}) /\ (S " {-infty}) is Element of K6(X)
((M " {+infty}) /\ (S " {+infty})) \/ ((M " {-infty}) /\ (S " {-infty})) is Element of K6(X)
((dom M) /\ (dom S)) \ (((M " {+infty}) /\ (S " {+infty})) \/ ((M " {-infty}) /\ (S " {-infty}))) is Element of K6(X)
M . E is ext-real Element of ExtREAL
S . E is ext-real Element of ExtREAL
(M . E) - (S . E) is ext-real Element of ExtREAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is set
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
M | S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
f is V11() real ext-real Element of REAL
f (#) M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(f (#) M) | S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
f (#) (M | S) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
E is Element of X
dom ((f (#) M) | S) is Element of K6(X)
K6(X) is non empty set
dom (f (#) M) is Element of K6(X)
(dom (f (#) M)) /\ S is Element of K6(X)
dom M is Element of K6(X)
(dom M) /\ S is Element of K6(X)
dom (M | S) is Element of K6(X)
dom (f (#) (M | S)) is Element of K6(X)
((f (#) M) | S) . E is ext-real Element of ExtREAL
(f (#) M) . E is ext-real Element of ExtREAL
R_EAL f is ext-real Element of ExtREAL
M . E is ext-real Element of ExtREAL
(R_EAL f) * (M . E) is ext-real Element of ExtREAL
(M | S) . E is ext-real Element of ExtREAL
(R_EAL f) * ((M | S) . E) is ext-real Element of ExtREAL
(f (#) (M | S)) . E is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
E - f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom E is Element of K6(X)
(dom f) /\ (dom E) is Element of K6(X)
(- 1) (#) f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((- 1) (#) f) is Element of K6(X)
(dom ((- 1) (#) f)) /\ (dom E) is Element of K6(X)
((- 1) (#) f) + E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(((- 1) (#) f) + E)) is ext-real Element of ExtREAL
max+ (((- 1) (#) f) + E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (((- 1) (#) f) + E))) is ext-real Element of ExtREAL
max- (((- 1) (#) f) + E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (((- 1) (#) f) + E))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((- 1) (#) f) + E)))) - (integral+ (M,(max- (((- 1) (#) f) + E)))) is ext-real Element of ExtREAL
b is Element of S
((- 1) (#) f) | b is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(((- 1) (#) f) | b)) is ext-real Element of ExtREAL
max+ (((- 1) (#) f) | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (((- 1) (#) f) | b))) is ext-real Element of ExtREAL
max- (((- 1) (#) f) | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (((- 1) (#) f) | b))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((- 1) (#) f) | b)))) - (integral+ (M,(max- (((- 1) (#) f) | b)))) is ext-real Element of ExtREAL
E | b is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(E | b)) is ext-real Element of ExtREAL
max+ (E | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (E | b))) is ext-real Element of ExtREAL
max- (E | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (E | b))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (E | b)))) - (integral+ (M,(max- (E | b)))) is ext-real Element of ExtREAL
(Integral (M,(((- 1) (#) f) | b))) + (Integral (M,(E | b))) is ext-real Element of ExtREAL
f | b is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f | b)) is ext-real Element of ExtREAL
max+ (f | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (f | b))) is ext-real Element of ExtREAL
max- (f | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (f | b))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (f | b)))) - (integral+ (M,(max- (f | b)))) is ext-real Element of ExtREAL
(- 1) (#) (f | b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
- f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
E + (- f) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
R_EAL (- 1) is ext-real Element of ExtREAL
(R_EAL (- 1)) * (Integral (M,(f | b))) is ext-real Element of ExtREAL
b1 is V11() real ext-real Element of REAL
(- 1) * b1 is V11() real ext-real Element of REAL
dom (((- 1) (#) f) + E) is Element of K6(X)
C is Element of S
E1 is Element of S
C is Element of S
((R_EAL (- 1)) * (Integral (M,(f | b)))) + (Integral (M,(E | b))) is ext-real Element of ExtREAL
- b1 is V11() real ext-real Element of REAL
a1 is V11() real ext-real Element of REAL
(- b1) + a1 is V11() real ext-real Element of REAL
0 + b1 is V11() real ext-real Element of REAL
((- b1) + a1) + b1 is V11() real ext-real Element of REAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
the Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|. the Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL)).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
M is set
dom |. the Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL)).| is Element of K6(X)
K6(X) is non empty set
|. the Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL)).| . M is ext-real Element of ExtREAL
the Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL)) . M is ext-real Element of ExtREAL
|.( the Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL)) . M).| is ext-real Element of ExtREAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.S.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
M is set
dom |.S.| is Element of K6(X)
K6(X) is non empty set
|.S.| . M is ext-real Element of ExtREAL
S . M is ext-real Element of ExtREAL
|.(S . M).| is ext-real Element of ExtREAL
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
K7(NAT,S) is non empty set
K6(K7(NAT,S)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
|.f.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
eq_dom (f,0.) is Element of K6(X)
(dom f) \ (eq_dom (f,0.)) is Element of K6(X)
E is Element of S
dom |.f.| is Element of K6(X)
a is set
E \ (eq_dom (f,0.)) is Element of K6(X)
b is Element of X
f . b is ext-real Element of ExtREAL
a1 is ext-real Element of ExtREAL
|.(f . b).| is ext-real Element of ExtREAL
|.f.| . b is ext-real Element of ExtREAL
great_dom (|.f.|,0.) is Element of K6(X)
E /\ (great_dom (|.f.|,0.)) is Element of K6(X)
a is set
b is Element of X
|.f.| . b is ext-real Element of ExtREAL
f . b is ext-real Element of ExtREAL
|.(f . b).| is ext-real Element of ExtREAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
a + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
1 / (a + 1) is V11() real ext-real non negative Element of REAL
K39((a + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((a + 1))) is V11() real ext-real non negative set
R_EAL (1 / (a + 1)) is ext-real Element of ExtREAL
great_eq_dom (|.f.|,(R_EAL (1 / (a + 1)))) is Element of K6(X)
E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (a + 1))))) is Element of K6(X)
a is Relation-like NAT -defined S -valued V18() V27( NAT ,S) Element of K6(K7(NAT,S))
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
a . b is Element of S
M . (a . b) is ext-real Element of ExtREAL
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
1 / (b + 1) is V11() real ext-real non negative Element of REAL
K39((b + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((b + 1))) is V11() real ext-real non negative set
R_EAL (1 / (b + 1)) is ext-real Element of ExtREAL
|.f.| | (a . b) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.f.| | E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
great_eq_dom (|.f.|,(R_EAL (1 / (b + 1)))) is Element of K6(X)
E /\ (great_eq_dom (|.f.|,(R_EAL (1 / (b + 1))))) is Element of K6(X)
dom (|.f.| | (a . b)) is Element of K6(X)
(dom |.f.|) /\ (a . b) is Element of K6(X)
E /\ (a . b) is M9(X,S)
integral+ (M,(|.f.| | (a . b))) is ext-real Element of ExtREAL
Integral (M,(|.f.| | (a . b))) is ext-real Element of ExtREAL
max+ (|.f.| | (a . b)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (|.f.| | (a . b)))) is ext-real Element of ExtREAL
max- (|.f.| | (a . b)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (|.f.| | (a . b)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (|.f.| | (a . b))))) - (integral+ (M,(max- (|.f.| | (a . b))))) is ext-real Element of ExtREAL
Integral (M,|.f.|) is ext-real Element of ExtREAL
max+ |.f.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ |.f.|)) is ext-real Element of ExtREAL
max- |.f.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- |.f.|)) is ext-real Element of ExtREAL
(integral+ (M,(max+ |.f.|))) - (integral+ (M,(max- |.f.|))) is ext-real Element of ExtREAL
(R_EAL (1 / (b + 1))) * (M . (a . b)) is ext-real Element of ExtREAL
((R_EAL (1 / (b + 1))) * (M . (a . b))) / (R_EAL (1 / (b + 1))) is ext-real Element of ExtREAL
E2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom E2 is Element of K6(X)
V1 is set
E2 . V1 is ext-real Element of ExtREAL
Integral (M,E2) is ext-real Element of ExtREAL
max+ E2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ E2)) is ext-real Element of ExtREAL
max- E2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- E2)) is ext-real Element of ExtREAL
(integral+ (M,(max+ E2))) - (integral+ (M,(max- E2))) is ext-real Element of ExtREAL
integral' (M,E2) is ext-real Element of ExtREAL
V1 is Element of X
E2 . V1 is ext-real Element of ExtREAL
(|.f.| | (a . b)) . V1 is ext-real Element of ExtREAL
|.f.| . V1 is ext-real Element of ExtREAL
integral+ (M,E2) is ext-real Element of ExtREAL
+infty / (R_EAL (1 / (b + 1))) is ext-real Element of ExtREAL
rng a is Element of K6(S)
K6(S) is non empty set
union (rng a) is set
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
a . b is Element of S
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
1 / (b + 1) is V11() real ext-real non negative Element of REAL
K39((b + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((b + 1))) is V11() real ext-real non negative set
0 + (1 / (b + 1)) is V11() real ext-real non negative Element of REAL
R_EAL (0 + (1 / (b + 1))) is ext-real Element of ExtREAL
great_eq_dom (|.f.|,(R_EAL (0 + (1 / (b + 1))))) is Element of K6(X)
E /\ (great_eq_dom (|.f.|,(R_EAL (0 + (1 / (b + 1)))))) is Element of K6(X)
R_EAL 0 is ext-real Element of ExtREAL
great_dom (|.f.|,(R_EAL 0)) is Element of K6(X)
E /\ (great_dom (|.f.|,(R_EAL 0))) is Element of K6(X)
b is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
a . b is Element of S
b + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
1 / (b + 1) is V11() real ext-real non negative Element of REAL
K39((b + 1)) is non empty V11() real ext-real positive non negative set
K37(1,K39((b + 1))) is V11() real ext-real non negative set
R_EAL (1 / (b + 1)) is ext-real Element of ExtREAL
great_eq_dom (|.f.|,(R_EAL (1 / (b + 1)))) is Element of K6(X)
(dom f) /\ (great_eq_dom (|.f.|,(R_EAL (1 / (b + 1))))) is Element of K6(X)
a1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
a . a1 is Element of S
b1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
a . b1 is Element of S
M . (a . b1) is ext-real Element of ExtREAL
the Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
K7(ExtREAL,ExtREAL) is non empty ext-real-valued set
K7(K7(ExtREAL,ExtREAL),ExtREAL) is non empty ext-real-valued set
K6(K7(K7(ExtREAL,ExtREAL),ExtREAL)) is non empty set
() is Relation-like K7(ExtREAL,ExtREAL) -defined ExtREAL -valued V18() V27(K7(ExtREAL,ExtREAL), ExtREAL ) ext-real-valued Element of K6(K7(K7(ExtREAL,ExtREAL),ExtREAL))
X is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
M is ext-real Element of ExtREAL
() . (S,M) is ext-real Element of ExtREAL
() . (X,(() . (S,M))) is ext-real Element of ExtREAL
() . (X,S) is ext-real Element of ExtREAL
() . ((() . (X,S)),M) is ext-real Element of ExtREAL
S * M is ext-real Element of ExtREAL
() . (X,(S * M)) is ext-real Element of ExtREAL
X * (S * M) is ext-real Element of ExtREAL
X * S is ext-real Element of ExtREAL
(X * S) * M is ext-real Element of ExtREAL
() . ((X * S),M) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
() . (X,S) is ext-real Element of ExtREAL
() . (S,X) is ext-real Element of ExtREAL
X * S is ext-real Element of ExtREAL
1. is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
() . (X,1.) is ext-real Element of ExtREAL
X * 1. is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
() . (1.,X) is ext-real Element of ExtREAL
1. * X is ext-real Element of ExtREAL
the_unity_wrt () is ext-real Element of ExtREAL
X is Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like ext-real-valued set
rng X is V76() set
S is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
() $$ S is ext-real Element of ExtREAL
f is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
S is ext-real Element of ExtREAL
() $$ f is ext-real Element of ExtREAL
E is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
M is ext-real Element of ExtREAL
() $$ E is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X is ext-real Element of ExtREAL
S |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of S -tuples_on ExtREAL
S -tuples_on ExtREAL is FinSequenceSet of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
X is ext-real Element of ExtREAL
S |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of S -tuples_on ExtREAL
S -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((S |-> X)) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,S) is set
S |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of S -tuples_on ExtREAL
S -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((S |-> X)) is ext-real Element of ExtREAL
<*> ExtREAL is empty proper epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real Relation-like NAT -defined ExtREAL -valued V18() V21() V34() FinSequence-like FinSubsequence-like FinSequence-membered ext-real non positive non negative complex-valued ext-real-valued real-valued natural-valued V75() V76() V77() V78() V79() V80() V81() FinSequence of ExtREAL
X is ext-real Element of ExtREAL
<*X*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
((<*> ExtREAL)) is ext-real Element of ExtREAL
() $$ (<*> ExtREAL) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
<*X*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
(<*X*>) is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
<*S*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
M is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
() $$ M is ext-real Element of ExtREAL
X is Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like ext-real-valued set
S is Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like ext-real-valued set
X ^ S is Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like set
rng (X ^ S) is set
rng X is V76() set
rng S is V76() set
(rng X) \/ (rng S) is V76() set
X is Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like ext-real-valued set
(X) is ext-real Element of ExtREAL
S is ext-real Element of ExtREAL
<*S*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
X ^ <*S*> is non empty Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like ext-real-valued set
((X ^ <*S*>)) is ext-real Element of ExtREAL
(X) * S is ext-real Element of ExtREAL
rng (X ^ <*S*>) is V76() set
rng X is V76() set
f is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
M is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
() $$ M is ext-real Element of ExtREAL
() $$ f is ext-real Element of ExtREAL
() . ((() $$ f),S) is ext-real Element of ExtREAL
E is Relation-like NAT -defined V18() V34() FinSequence-like FinSubsequence-like ext-real-valued set
(E) is ext-real Element of ExtREAL
() . ((E),S) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
(X,1) is ext-real Element of ExtREAL
1 |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 1 -tuples_on ExtREAL
1 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((1 |-> X)) is ext-real Element of ExtREAL
<*X*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
(<*X*>) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,(S + 1)) is ext-real Element of ExtREAL
(S + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (S + 1) -tuples_on ExtREAL
(S + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((S + 1) |-> X)) is ext-real Element of ExtREAL
(X,S) is ext-real Element of ExtREAL
S |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of S -tuples_on ExtREAL
S -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((S |-> X)) is ext-real Element of ExtREAL
(X,S) * X is ext-real Element of ExtREAL
(S + 1) + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,((S + 1) + 1)) is ext-real Element of ExtREAL
((S + 1) + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of ((S + 1) + 1) -tuples_on ExtREAL
((S + 1) + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((((S + 1) + 1) |-> X)) is ext-real Element of ExtREAL
(X,(S + 1)) * X is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(M + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (M + 1) -tuples_on ExtREAL
(M + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((M + 1) |-> X)) is ext-real Element of ExtREAL
M |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of M -tuples_on ExtREAL
M -tuples_on ExtREAL is FinSequenceSet of ExtREAL
<*X*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
(M |-> X) ^ <*X*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
(((M |-> X) ^ <*X*>)) is ext-real Element of ExtREAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,(0 + 1)) is ext-real Element of ExtREAL
(0 + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (0 + 1) -tuples_on ExtREAL
(0 + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((0 + 1) |-> X)) is ext-real Element of ExtREAL
<*X*> is non empty Relation-like NAT -defined ExtREAL -valued V18() V34() V41(1) FinSequence-like FinSubsequence-like ext-real-valued FinSequence of ExtREAL
(<*X*>) is ext-real Element of ExtREAL
1. * X is ext-real Element of ExtREAL
0 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,(0 + 1)) is ext-real Element of ExtREAL
(0 + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (0 + 1) -tuples_on ExtREAL
(0 + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((0 + 1) |-> X)) is ext-real Element of ExtREAL
(X,0) is ext-real Element of ExtREAL
0 |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 0 -tuples_on ExtREAL
0 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((0 |-> X)) is ext-real Element of ExtREAL
(X,0) * X is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
S + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,(S + 1)) is ext-real Element of ExtREAL
(S + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (S + 1) -tuples_on ExtREAL
(S + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((S + 1) |-> X)) is ext-real Element of ExtREAL
(X,S) is ext-real Element of ExtREAL
S |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of S -tuples_on ExtREAL
S -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((S |-> X)) is ext-real Element of ExtREAL
(X,S) * X is ext-real Element of ExtREAL
S is non empty set
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(S,ExtREAL))
dom M is Element of K6(S)
K6(S) is non empty set
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
f is Relation-like S -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(S,ExtREAL))
dom f is Element of K6(S)
E is set
E is set
E is Element of S
f . E is ext-real Element of ExtREAL
M . E is ext-real Element of ExtREAL
((M . E),X) is ext-real Element of ExtREAL
X |-> (M . E) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (M . E))) is ext-real Element of ExtREAL
f /. E is ext-real Element of ExtREAL
f is Relation-like S -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(S,ExtREAL))
dom f is Element of K6(S)
E is Relation-like S -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(S,ExtREAL))
dom E is Element of K6(S)
a is Element of S
f . a is ext-real Element of ExtREAL
E . a is ext-real Element of ExtREAL
M . a is ext-real Element of ExtREAL
((M . a),X) is ext-real Element of ExtREAL
X |-> (M . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (M . a))) is ext-real Element of ExtREAL
X is ext-real Element of ExtREAL
S is V11() real ext-real set
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,M) is ext-real Element of ExtREAL
M |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of M -tuples_on ExtREAL
M -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((M |-> X)) is ext-real Element of ExtREAL
S |^ M is set
E is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,E) is ext-real Element of ExtREAL
E |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of E -tuples_on ExtREAL
E -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((E |-> X)) is ext-real Element of ExtREAL
S |^ E is set
E + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,(E + 1)) is ext-real Element of ExtREAL
(E + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (E + 1) -tuples_on ExtREAL
(E + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((E + 1) |-> X)) is ext-real Element of ExtREAL
S |^ (E + 1) is set
(X,E) * X is ext-real Element of ExtREAL
f is V11() real ext-real Element of REAL
f |^ E is V11() real ext-real Element of REAL
(f |^ E) * f is V11() real ext-real Element of REAL
(X,0) is ext-real Element of ExtREAL
0 |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 0 -tuples_on ExtREAL
0 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((0 |-> X)) is ext-real Element of ExtREAL
S |^ 0 is set
X is ext-real Element of ExtREAL
S is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,S) is ext-real Element of ExtREAL
S |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of S -tuples_on ExtREAL
S -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((S |-> X)) is ext-real Element of ExtREAL
M is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(X,M) is ext-real Element of ExtREAL
M |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of M -tuples_on ExtREAL
M -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((M |-> X)) is ext-real Element of ExtREAL
M + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X,(M + 1)) is ext-real Element of ExtREAL
(M + 1) |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (M + 1) -tuples_on ExtREAL
(M + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((M + 1) |-> X)) is ext-real Element of ExtREAL
(X,M) * X is ext-real Element of ExtREAL
(X,0) is ext-real Element of ExtREAL
0 |-> X is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 0 -tuples_on ExtREAL
0 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((0 |-> X)) is ext-real Element of ExtREAL
X is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative set
(+infty,X) is ext-real Element of ExtREAL
X |-> +infty is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> +infty)) is ext-real Element of ExtREAL
X + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(+infty,(X + 1)) is ext-real Element of ExtREAL
(X + 1) |-> +infty is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (X + 1) -tuples_on ExtREAL
(X + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((X + 1) |-> +infty)) is ext-real Element of ExtREAL
(+infty,X) * +infty is ext-real Element of ExtREAL
(+infty,1) is ext-real Element of ExtREAL
1 |-> +infty is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 1 -tuples_on ExtREAL
1 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((1 |-> +infty)) is ext-real Element of ExtREAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
(+infty,X) is ext-real Element of ExtREAL
X |-> +infty is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> +infty)) is ext-real Element of ExtREAL
X is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative set
S is non empty set
K6(S) is non empty set
K6(K6(S)) is non empty set
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(S))
f is Relation-like S -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(S,ExtREAL))
dom f is Element of K6(S)
|.f.| is Relation-like S -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(S,ExtREAL))
(X,S,|.f.|) is Relation-like S -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(S,ExtREAL))
E is Element of M
dom (X,S,|.f.|) is Element of K6(S)
dom |.f.| is Element of K6(S)
b is V11() real ext-real set
R_EAL b is ext-real Element of ExtREAL
less_dom ((X,S,|.f.|),(R_EAL b)) is Element of K6(S)
E /\ (less_dom ((X,S,|.f.|),(R_EAL b))) is Element of K6(S)
a1 is set
(X,S,|.f.|) . a1 is ext-real Element of ExtREAL
|.f.| . a1 is ext-real Element of ExtREAL
((|.f.| . a1),X) is ext-real Element of ExtREAL
X |-> (|.f.| . a1) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (|.f.| . a1))) is ext-real Element of ExtREAL
b is V11() real ext-real set
R_EAL b is ext-real Element of ExtREAL
less_dom ((X,S,|.f.|),(R_EAL b)) is Element of K6(S)
E /\ (less_dom ((X,S,|.f.|),(R_EAL b))) is Element of K6(S)
great_eq_dom ((X,S,|.f.|),(R_EAL b)) is Element of K6(S)
a1 is set
(X,S,|.f.|) . a1 is ext-real Element of ExtREAL
|.f.| . a1 is ext-real Element of ExtREAL
((|.f.| . a1),X) is ext-real Element of ExtREAL
X |-> (|.f.| . a1) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (|.f.| . a1))) is ext-real Element of ExtREAL
E /\ (great_eq_dom ((X,S,|.f.|),(R_EAL b))) is Element of K6(S)
E \ E is M9(S,M)
1 / X is V11() real ext-real non negative Element of REAL
K39(X) is V11() real ext-real non negative set
K37(1,K39(X)) is V11() real ext-real non negative set
(1 / X) * X is V11() real ext-real non negative Element of REAL
b is V11() real ext-real set
R_EAL b is ext-real Element of ExtREAL
great_eq_dom ((X,S,|.f.|),(R_EAL b)) is Element of K6(S)
b to_power (1 / X) is V11() real ext-real set
R_EAL (b to_power (1 / X)) is ext-real Element of ExtREAL
great_eq_dom (|.f.|,(R_EAL (b to_power (1 / X)))) is Element of K6(S)
a1 is set
|.f.| . a1 is ext-real Element of ExtREAL
f . a1 is ext-real Element of ExtREAL
|.(f . a1).| is ext-real Element of ExtREAL
(X,S,|.f.|) . a1 is ext-real Element of ExtREAL
((|.f.| . a1),X) is ext-real Element of ExtREAL
X |-> (|.f.| . a1) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (|.f.| . a1))) is ext-real Element of ExtREAL
b1 is V11() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
b1 to_power a is V11() real ext-real Element of REAL
b1 |^ a is set
b1 to_power X is V11() real ext-real set
b1 |^ X is set
(b1 to_power X) to_power (1 / X) is V11() real ext-real set
X * 1 is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
(X * 1) / X is V11() real ext-real non negative Element of REAL
K37((X * 1),K39(X)) is V11() real ext-real non negative set
b1 to_power ((X * 1) / X) is V11() real ext-real Element of REAL
a1 is set
(X,S,|.f.|) . a1 is ext-real Element of ExtREAL
|.f.| . a1 is ext-real Element of ExtREAL
((|.f.| . a1),X) is ext-real Element of ExtREAL
X |-> (|.f.| . a1) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (|.f.| . a1))) is ext-real Element of ExtREAL
f . a1 is ext-real Element of ExtREAL
|.(f . a1).| is ext-real Element of ExtREAL
C is V11() real ext-real Element of REAL
a is epsilon-transitive epsilon-connected ordinal natural V11() real ext-real non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
C to_power a is V11() real ext-real Element of REAL
C |^ a is set
b to_power ((1 / X) * X) is V11() real ext-real set
b1 is V11() real ext-real Element of REAL
b1 |^ X is V11() real ext-real Element of REAL
b to_power 1 is V11() real ext-real set
b |^ 1 is set
b1 to_power X is V11() real ext-real set
b1 |^ X is set
b is V11() real ext-real set
R_EAL b is ext-real Element of ExtREAL
great_eq_dom ((X,S,|.f.|),(R_EAL b)) is Element of K6(S)
E /\ (great_eq_dom ((X,S,|.f.|),(R_EAL b))) is Element of K6(S)
a1 is set
|.f.| . a1 is ext-real Element of ExtREAL
f . a1 is ext-real Element of ExtREAL
|.(f . a1).| is ext-real Element of ExtREAL
(X,S,|.f.|) . a1 is ext-real Element of ExtREAL
((|.f.| . a1),X) is ext-real Element of ExtREAL
X |-> (|.f.| . a1) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of X -tuples_on ExtREAL
X -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((X |-> (|.f.| . a1))) is ext-real Element of ExtREAL
b to_power (1 / X) is V11() real ext-real set
R_EAL (b to_power (1 / X)) is ext-real Element of ExtREAL
great_eq_dom (|.f.|,(R_EAL (b to_power (1 / X)))) is Element of K6(S)
E /\ (great_eq_dom (|.f.|,(R_EAL (b to_power (1 / X))))) is Element of K6(S)
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom M is Element of K6(X)
f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
(dom M) /\ (dom f) is Element of K6(X)
M (#) f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
E is Element of S
dom (M (#) f) is Element of K6(X)
M + f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(M + f).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
(2,X,|.(M + f).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
4 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
1 / 4 is V11() real ext-real non negative Element of REAL
K39(4) is non empty V11() real ext-real positive non negative set
K37(1,K39(4)) is V11() real ext-real non negative set
(1 / 4) (#) (2,X,|.(M + f).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((1 / 4) (#) (2,X,|.(M + f).|)) is Element of K6(X)
dom (2,X,|.(M + f).|) is Element of K6(X)
M - f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(M - f).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
(2,X,|.(M - f).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (2,X,|.(M - f).|) is Element of K6(X)
dom |.(M - f).| is Element of K6(X)
dom (M - f) is Element of K6(X)
(1 / 4) (#) (2,X,|.(M - f).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((1 / 4) (#) (2,X,|.(M - f).|)) is Element of K6(X)
dom |.(M + f).| is Element of K6(X)
dom (M + f) is Element of K6(X)
a is Element of X
(2,X,|.(M + f).|) . a is ext-real Element of ExtREAL
|.((2,X,|.(M + f).|) . a).| is ext-real Element of ExtREAL
f . a is ext-real Element of ExtREAL
|.(f . a).| is ext-real Element of ExtREAL
M . a is ext-real Element of ExtREAL
|.(M . a).| is ext-real Element of ExtREAL
(M . a) + (f . a) is ext-real Element of ExtREAL
b is V11() real ext-real Element of REAL
a1 is V11() real ext-real Element of REAL
b + a1 is V11() real ext-real Element of REAL
|.((M . a) + (f . a)).| is ext-real Element of ExtREAL
abs (b + a1) is V11() real ext-real Element of REAL
|.((M . a) + (f . a)).| * |.((M . a) + (f . a)).| is ext-real Element of ExtREAL
(abs (b + a1)) * (abs (b + a1)) is V11() real ext-real Element of REAL
|.(M + f).| . a is ext-real Element of ExtREAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
((|.(M + f).| . a),(1 + 1)) is ext-real Element of ExtREAL
(1 + 1) |-> (|.(M + f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (1 + 1) -tuples_on ExtREAL
(1 + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((1 + 1) |-> (|.(M + f).| . a))) is ext-real Element of ExtREAL
((|.(M + f).| . a),1) is ext-real Element of ExtREAL
1 |-> (|.(M + f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 1 -tuples_on ExtREAL
1 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((1 |-> (|.(M + f).| . a))) is ext-real Element of ExtREAL
((|.(M + f).| . a),1) * (|.(M + f).| . a) is ext-real Element of ExtREAL
(M + f) . a is ext-real Element of ExtREAL
|.((M + f) . a).| is ext-real Element of ExtREAL
|.(|.((M . a) + (f . a)).| * |.((M . a) + (f . a)).|).| is ext-real Element of ExtREAL
((M . a) + (f . a)) * ((M . a) + (f . a)) is ext-real Element of ExtREAL
|.(((M . a) + (f . a)) * ((M . a) + (f . a))).| is ext-real Element of ExtREAL
|.|.(((M . a) + (f . a)) * ((M . a) + (f . a))).|.| is ext-real Element of ExtREAL
((1 / 4) (#) (2,X,|.(M + f).|)) - ((1 / 4) (#) (2,X,|.(M - f).|)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (((1 / 4) (#) (2,X,|.(M + f).|)) - ((1 / 4) (#) (2,X,|.(M - f).|))) is Element of K6(X)
(dom ((1 / 4) (#) (2,X,|.(M + f).|))) /\ (dom ((1 / 4) (#) (2,X,|.(M - f).|))) is Element of K6(X)
a is Element of X
(M (#) f) . a is ext-real Element of ExtREAL
(((1 / 4) (#) (2,X,|.(M + f).|)) - ((1 / 4) (#) (2,X,|.(M - f).|))) . a is ext-real Element of ExtREAL
f . a is ext-real Element of ExtREAL
|.(f . a).| is ext-real Element of ExtREAL
M . a is ext-real Element of ExtREAL
|.(M . a).| is ext-real Element of ExtREAL
(M . a) + (f . a) is ext-real Element of ExtREAL
b is V11() real ext-real Element of REAL
a1 is V11() real ext-real Element of REAL
b + a1 is V11() real ext-real Element of REAL
|.((M . a) + (f . a)).| is ext-real Element of ExtREAL
abs (b + a1) is V11() real ext-real Element of REAL
|.((M . a) + (f . a)).| * |.((M . a) + (f . a)).| is ext-real Element of ExtREAL
(abs (b + a1)) * (abs (b + a1)) is V11() real ext-real Element of REAL
((1 / 4) (#) (2,X,|.(M + f).|)) . a is ext-real Element of ExtREAL
R_EAL (1 / 4) is ext-real Element of ExtREAL
(2,X,|.(M + f).|) . a is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * ((2,X,|.(M + f).|) . a) is ext-real Element of ExtREAL
|.(M + f).| . a is ext-real Element of ExtREAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
((|.(M + f).| . a),(1 + 1)) is ext-real Element of ExtREAL
(1 + 1) |-> (|.(M + f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (1 + 1) -tuples_on ExtREAL
(1 + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((1 + 1) |-> (|.(M + f).| . a))) is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * ((|.(M + f).| . a),(1 + 1)) is ext-real Element of ExtREAL
((|.(M + f).| . a),1) is ext-real Element of ExtREAL
1 |-> (|.(M + f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 1 -tuples_on ExtREAL
1 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((1 |-> (|.(M + f).| . a))) is ext-real Element of ExtREAL
((|.(M + f).| . a),1) * (|.(M + f).| . a) is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * (((|.(M + f).| . a),1) * (|.(M + f).| . a)) is ext-real Element of ExtREAL
(M + f) . a is ext-real Element of ExtREAL
|.((M + f) . a).| is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * (|.((M . a) + (f . a)).| * |.((M . a) + (f . a)).|) is ext-real Element of ExtREAL
(1 / 4) * ((abs (b + a1)) * (abs (b + a1))) is V11() real ext-real Element of REAL
b - a1 is V11() real ext-real Element of REAL
K38(a1) is V11() real ext-real set
K36(b,K38(a1)) is V11() real ext-real set
abs (b - a1) is V11() real ext-real Element of REAL
(abs (b - a1)) * (abs (b - a1)) is V11() real ext-real Element of REAL
(abs (b - a1)) ^2 is V11() real ext-real Element of REAL
K37((abs (b - a1)),(abs (b - a1))) is V11() real ext-real set
(b - a1) ^2 is V11() real ext-real Element of REAL
K37((b - a1),(b - a1)) is V11() real ext-real set
((1 / 4) (#) (2,X,|.(M - f).|)) . a is ext-real Element of ExtREAL
(2,X,|.(M - f).|) . a is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * ((2,X,|.(M - f).|) . a) is ext-real Element of ExtREAL
|.(M - f).| . a is ext-real Element of ExtREAL
((|.(M - f).| . a),(1 + 1)) is ext-real Element of ExtREAL
(1 + 1) |-> (|.(M - f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (1 + 1) -tuples_on ExtREAL
(((1 + 1) |-> (|.(M - f).| . a))) is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * ((|.(M - f).| . a),(1 + 1)) is ext-real Element of ExtREAL
((|.(M - f).| . a),1) is ext-real Element of ExtREAL
1 |-> (|.(M - f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 1 -tuples_on ExtREAL
((1 |-> (|.(M - f).| . a))) is ext-real Element of ExtREAL
((|.(M - f).| . a),1) * (|.(M - f).| . a) is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * (((|.(M - f).| . a),1) * (|.(M - f).| . a)) is ext-real Element of ExtREAL
(M . a) - (f . a) is ext-real Element of ExtREAL
|.((M . a) - (f . a)).| is ext-real Element of ExtREAL
|.((M . a) - (f . a)).| * |.((M . a) - (f . a)).| is ext-real Element of ExtREAL
(M - f) . a is ext-real Element of ExtREAL
|.((M - f) . a).| is ext-real Element of ExtREAL
(R_EAL (1 / 4)) * (|.((M . a) - (f . a)).| * |.((M . a) - (f . a)).|) is ext-real Element of ExtREAL
(1 / 4) * ((abs (b - a1)) * (abs (b - a1))) is V11() real ext-real Element of REAL
(abs (b + a1)) ^2 is V11() real ext-real Element of REAL
K37((abs (b + a1)),(abs (b + a1))) is V11() real ext-real set
(b + a1) ^2 is V11() real ext-real Element of REAL
K37((b + a1),(b + a1)) is V11() real ext-real set
(((1 / 4) (#) (2,X,|.(M + f).|)) . a) - (((1 / 4) (#) (2,X,|.(M - f).|)) . a) is ext-real Element of ExtREAL
b ^2 is V11() real ext-real Element of REAL
K37(b,b) is V11() real ext-real set
2 * b is V11() real ext-real Element of REAL
(2 * b) * a1 is V11() real ext-real Element of REAL
(b ^2) + ((2 * b) * a1) is V11() real ext-real Element of REAL
a1 ^2 is V11() real ext-real Element of REAL
K37(a1,a1) is V11() real ext-real set
((b ^2) + ((2 * b) * a1)) + (a1 ^2) is V11() real ext-real Element of REAL
(1 / 4) * (((b ^2) + ((2 * b) * a1)) + (a1 ^2)) is V11() real ext-real Element of REAL
(b ^2) - ((2 * b) * a1) is V11() real ext-real Element of REAL
K38(((2 * b) * a1)) is V11() real ext-real set
K36((b ^2),K38(((2 * b) * a1))) is V11() real ext-real set
((b ^2) - ((2 * b) * a1)) + (a1 ^2) is V11() real ext-real Element of REAL
(1 / 4) * (((b ^2) - ((2 * b) * a1)) + (a1 ^2)) is V11() real ext-real Element of REAL
((1 / 4) * (((b ^2) + ((2 * b) * a1)) + (a1 ^2))) - ((1 / 4) * (((b ^2) - ((2 * b) * a1)) + (a1 ^2))) is V11() real ext-real Element of REAL
K38(((1 / 4) * (((b ^2) - ((2 * b) * a1)) + (a1 ^2)))) is V11() real ext-real set
K36(((1 / 4) * (((b ^2) + ((2 * b) * a1)) + (a1 ^2))),K38(((1 / 4) * (((b ^2) - ((2 * b) * a1)) + (a1 ^2))))) is V11() real ext-real set
b * a1 is V11() real ext-real Element of REAL
(M . a) * (f . a) is ext-real Element of ExtREAL
a is Element of X
(2,X,|.(M - f).|) . a is ext-real Element of ExtREAL
|.((2,X,|.(M - f).|) . a).| is ext-real Element of ExtREAL
f . a is ext-real Element of ExtREAL
|.(f . a).| is ext-real Element of ExtREAL
M . a is ext-real Element of ExtREAL
|.(M . a).| is ext-real Element of ExtREAL
(M . a) - (f . a) is ext-real Element of ExtREAL
b is V11() real ext-real Element of REAL
a1 is V11() real ext-real Element of REAL
b - a1 is V11() real ext-real Element of REAL
K38(a1) is V11() real ext-real set
K36(b,K38(a1)) is V11() real ext-real set
|.((M . a) - (f . a)).| is ext-real Element of ExtREAL
abs (b - a1) is V11() real ext-real Element of REAL
|.((M . a) - (f . a)).| * |.((M . a) - (f . a)).| is ext-real Element of ExtREAL
(abs (b - a1)) * (abs (b - a1)) is V11() real ext-real Element of REAL
|.(M - f).| . a is ext-real Element of ExtREAL
1 + 1 is non empty epsilon-transitive epsilon-connected ordinal natural V11() real ext-real positive non negative V51() V75() V76() V77() V78() V79() V80() V84() Element of NAT
((|.(M - f).| . a),(1 + 1)) is ext-real Element of ExtREAL
(1 + 1) |-> (|.(M - f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of (1 + 1) -tuples_on ExtREAL
(1 + 1) -tuples_on ExtREAL is FinSequenceSet of ExtREAL
(((1 + 1) |-> (|.(M - f).| . a))) is ext-real Element of ExtREAL
((|.(M - f).| . a),1) is ext-real Element of ExtREAL
1 |-> (|.(M - f).| . a) is Relation-like NAT -defined ExtREAL -valued V18() V34() FinSequence-like FinSubsequence-like ext-real-valued Element of 1 -tuples_on ExtREAL
1 -tuples_on ExtREAL is FinSequenceSet of ExtREAL
((1 |-> (|.(M - f).| . a))) is ext-real Element of ExtREAL
((|.(M - f).| . a),1) * (|.(M - f).| . a) is ext-real Element of ExtREAL
(M - f) . a is ext-real Element of ExtREAL
|.((M - f) . a).| is ext-real Element of ExtREAL
|.(|.((M . a) - (f . a)).| * |.((M . a) - (f . a)).|).| is ext-real Element of ExtREAL
((M . a) - (f . a)) * ((M . a) - (f . a)) is ext-real Element of ExtREAL
|.(((M . a) - (f . a)) * ((M . a) - (f . a))).| is ext-real Element of ExtREAL
|.|.(((M . a) - (f . a)) * ((M . a) - (f . a))).|.| is ext-real Element of ExtREAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
rng S is V76() Element of K6(ExtREAL)
M is V11() real ext-real set
f is V11() real ext-real set
E is Element of X
dom S is Element of K6(X)
K6(X) is non empty set
S . E is ext-real Element of ExtREAL
- +infty is non empty ext-real non positive negative Element of ExtREAL
|.(S . E).| is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom E is Element of K6(X)
(dom f) /\ (dom E) is Element of K6(X)
rng f is V76() Element of K6(ExtREAL)
f (#) E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
f (#) |.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
a is Element of S
(f (#) E) | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(f (#) |.E.|) | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((f (#) |.E.|) | a)) is ext-real Element of ExtREAL
max+ ((f (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((f (#) |.E.|) | a))) is ext-real Element of ExtREAL
max- ((f (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((f (#) |.E.|) | a))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((f (#) |.E.|) | a)))) - (integral+ (M,(max- ((f (#) |.E.|) | a)))) is ext-real Element of ExtREAL
|.E.| | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(|.E.| | a)) is ext-real Element of ExtREAL
max+ (|.E.| | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (|.E.| | a))) is ext-real Element of ExtREAL
max- (|.E.| | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (|.E.| | a))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (|.E.| | a)))) - (integral+ (M,(max- (|.E.| | a)))) is ext-real Element of ExtREAL
b is non empty V76() Element of K6(ExtREAL)
inf b is ext-real Element of ExtREAL
sup b is ext-real Element of ExtREAL
dom ((f (#) |.E.|) | a) is Element of K6(X)
dom (f (#) |.E.|) is Element of K6(X)
(dom (f (#) |.E.|)) /\ a is Element of K6(X)
|.(sup b).| is ext-real Element of ExtREAL
b1 is V11() real ext-real Element of REAL
abs b1 is V11() real ext-real Element of REAL
|.(inf b).| is ext-real Element of ExtREAL
a1 is V11() real ext-real Element of REAL
abs a1 is V11() real ext-real Element of REAL
dom |.E.| is Element of K6(X)
E2 is Element of X
|.E.| . E2 is ext-real Element of ExtREAL
|.(|.E.| . E2).| is ext-real Element of ExtREAL
E . E2 is ext-real Element of ExtREAL
|.(E . E2).| is ext-real Element of ExtREAL
|.|.(E . E2).|.| is ext-real Element of ExtREAL
E2 is Element of S
(dom f) /\ (dom |.E.|) is Element of K6(X)
a1 (#) |.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (a1 (#) |.E.|) is Element of K6(X)
(a1 (#) |.E.|) | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((a1 (#) |.E.|) | a) is Element of K6(X)
V1 is Element of X
E . V1 is ext-real Element of ExtREAL
|.(E . V1).| is ext-real Element of ExtREAL
(inf b) * |.(E . V1).| is ext-real Element of ExtREAL
f . V1 is ext-real Element of ExtREAL
(f . V1) * |.(E . V1).| is ext-real Element of ExtREAL
(sup b) * |.(E . V1).| is ext-real Element of ExtREAL
V1 is Element of X
((a1 (#) |.E.|) | a) . V1 is ext-real Element of ExtREAL
((f (#) |.E.|) | a) . V1 is ext-real Element of ExtREAL
(a1 (#) |.E.|) . V1 is ext-real Element of ExtREAL
(f (#) |.E.|) . V1 is ext-real Element of ExtREAL
f . V1 is ext-real Element of ExtREAL
|.E.| . V1 is ext-real Element of ExtREAL
(f . V1) * (|.E.| . V1) is ext-real Element of ExtREAL
E . V1 is ext-real Element of ExtREAL
|.(E . V1).| is ext-real Element of ExtREAL
(f . V1) * |.(E . V1).| is ext-real Element of ExtREAL
R_EAL a1 is ext-real Element of ExtREAL
(R_EAL a1) * (|.E.| . V1) is ext-real Element of ExtREAL
(R_EAL a1) * |.(E . V1).| is ext-real Element of ExtREAL
((f (#) |.E.|) | a) - ((a1 (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
b1 (#) |.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (b1 (#) |.E.|) is Element of K6(X)
(b1 (#) |.E.|) | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((b1 (#) |.E.|) | a) is Element of K6(X)
dom (f (#) E) is Element of K6(X)
dom ((f (#) E) | a) is Element of K6(X)
|.((f (#) E) | a).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom |.((f (#) E) | a).| is Element of K6(X)
V1 is Element of X
((f (#) |.E.|) | a) . V1 is ext-real Element of ExtREAL
|.(((f (#) |.E.|) | a) . V1).| is ext-real Element of ExtREAL
|.((f (#) E) | a).| . V1 is ext-real Element of ExtREAL
(f (#) |.E.|) . V1 is ext-real Element of ExtREAL
|.((f (#) |.E.|) . V1).| is ext-real Element of ExtREAL
f . V1 is ext-real Element of ExtREAL
|.E.| . V1 is ext-real Element of ExtREAL
(f . V1) * (|.E.| . V1) is ext-real Element of ExtREAL
|.((f . V1) * (|.E.| . V1)).| is ext-real Element of ExtREAL
E . V1 is ext-real Element of ExtREAL
|.(E . V1).| is ext-real Element of ExtREAL
(f . V1) * |.(E . V1).| is ext-real Element of ExtREAL
|.((f . V1) * |.(E . V1).|).| is ext-real Element of ExtREAL
|.(f . V1).| is ext-real Element of ExtREAL
|.|.(E . V1).|.| is ext-real Element of ExtREAL
|.(f . V1).| * |.|.(E . V1).|.| is ext-real Element of ExtREAL
|.(f . V1).| * |.(E . V1).| is ext-real Element of ExtREAL
(f . V1) * (E . V1) is ext-real Element of ExtREAL
|.((f . V1) * (E . V1)).| is ext-real Element of ExtREAL
|.(f (#) E).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom |.(f (#) E).| is Element of K6(X)
|.(f (#) E).| . V1 is ext-real Element of ExtREAL
(f (#) E) . V1 is ext-real Element of ExtREAL
|.((f (#) E) . V1).| is ext-real Element of ExtREAL
((f (#) E) | a) . V1 is ext-real Element of ExtREAL
|.(((f (#) E) | a) . V1).| is ext-real Element of ExtREAL
Integral (M,((b1 (#) |.E.|) | a)) is ext-real Element of ExtREAL
max+ ((b1 (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((b1 (#) |.E.|) | a))) is ext-real Element of ExtREAL
max- ((b1 (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((b1 (#) |.E.|) | a))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((b1 (#) |.E.|) | a)))) - (integral+ (M,(max- ((b1 (#) |.E.|) | a)))) is ext-real Element of ExtREAL
b1 (#) (|.E.| | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(b1 (#) (|.E.| | a))) is ext-real Element of ExtREAL
max+ (b1 (#) (|.E.| | a)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (b1 (#) (|.E.| | a)))) is ext-real Element of ExtREAL
max- (b1 (#) (|.E.| | a)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (b1 (#) (|.E.| | a)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (b1 (#) (|.E.| | a))))) - (integral+ (M,(max- (b1 (#) (|.E.| | a))))) is ext-real Element of ExtREAL
R_EAL b1 is ext-real Element of ExtREAL
(R_EAL b1) * (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
(dom (f (#) E)) /\ a is Element of K6(X)
|.(inf b).| + |.(sup b).| is ext-real Element of ExtREAL
b1 + 0 is V11() real ext-real Element of REAL
b1 + (abs a1) is V11() real ext-real Element of REAL
(abs b1) + (abs a1) is V11() real ext-real Element of REAL
- (abs a1) is V11() real ext-real Element of REAL
(- (abs a1)) - (abs b1) is V11() real ext-real Element of REAL
K38((abs b1)) is V11() real ext-real set
K36((- (abs a1)),K38((abs b1))) is V11() real ext-real set
(- (abs a1)) - 0 is V11() real ext-real Element of REAL
K38(0) is empty epsilon-transitive epsilon-connected ordinal T-Sequence-like c=-linear natural V11() real V21() FinSequence-membered ext-real non positive non negative V75() V76() V77() V78() V79() V80() V81() set
K36((- (abs a1)),K38(0)) is V11() real ext-real set
V1 is Element of X
f . V1 is ext-real Element of ExtREAL
|.(f . V1).| is ext-real Element of ExtREAL
V2 is V11() real ext-real Element of REAL
(abs a1) + (abs b1) is V11() real ext-real Element of REAL
- ((abs a1) + (abs b1)) is V11() real ext-real Element of REAL
abs V2 is V11() real ext-real Element of REAL
C is V11() real ext-real Element of REAL
E1 is V11() real ext-real Element of REAL
C + E1 is V11() real ext-real Element of REAL
(C + E1) (#) |.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
((C + E1) (#) |.E.|) | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (((C + E1) (#) |.E.|) | a) is Element of K6(X)
(C + E1) (#) (|.E.| | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((C + E1) (#) (|.E.| | a)) is Element of K6(X)
dom (|.E.| | a) is Element of K6(X)
dom ((C + E1) (#) |.E.|) is Element of K6(X)
V1 is Element of X
((f (#) E) | a) . V1 is ext-real Element of ExtREAL
|.(((f (#) E) | a) . V1).| is ext-real Element of ExtREAL
(((C + E1) (#) |.E.|) | a) . V1 is ext-real Element of ExtREAL
(f (#) E) . V1 is ext-real Element of ExtREAL
f | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (f | a) is Element of K6(X)
(f | a) . V1 is ext-real Element of ExtREAL
f . V1 is ext-real Element of ExtREAL
E | a is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (E | a) is Element of K6(X)
(E | a) . V1 is ext-real Element of ExtREAL
E . V1 is ext-real Element of ExtREAL
|.((E | a) . V1).| is ext-real Element of ExtREAL
|.((f | a) . V1).| is ext-real Element of ExtREAL
|.((f | a) . V1).| * |.((E | a) . V1).| is ext-real Element of ExtREAL
(|.(inf b).| + |.(sup b).|) * |.((E | a) . V1).| is ext-real Element of ExtREAL
((C + E1) (#) |.E.|) . V1 is ext-real Element of ExtREAL
|.((f (#) E) . V1).| is ext-real Element of ExtREAL
(f . V1) * (E . V1) is ext-real Element of ExtREAL
|.((f . V1) * (E . V1)).| is ext-real Element of ExtREAL
R_EAL (C + E1) is ext-real Element of ExtREAL
|.E.| . V1 is ext-real Element of ExtREAL
(R_EAL (C + E1)) * (|.E.| . V1) is ext-real Element of ExtREAL
(R_EAL (C + E1)) * |.((E | a) . V1).| is ext-real Element of ExtREAL
(dom ((a1 (#) |.E.|) | a)) /\ (dom ((f (#) |.E.|) | a)) is Element of K6(X)
V1 is Element of S
((a1 (#) |.E.|) | a) | V1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(((a1 (#) |.E.|) | a) | V1)) is ext-real Element of ExtREAL
max+ (((a1 (#) |.E.|) | a) | V1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (((a1 (#) |.E.|) | a) | V1))) is ext-real Element of ExtREAL
max- (((a1 (#) |.E.|) | a) | V1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (((a1 (#) |.E.|) | a) | V1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((a1 (#) |.E.|) | a) | V1)))) - (integral+ (M,(max- (((a1 (#) |.E.|) | a) | V1)))) is ext-real Element of ExtREAL
((f (#) |.E.|) | a) | V1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(((f (#) |.E.|) | a) | V1)) is ext-real Element of ExtREAL
max+ (((f (#) |.E.|) | a) | V1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (((f (#) |.E.|) | a) | V1))) is ext-real Element of ExtREAL
max- (((f (#) |.E.|) | a) | V1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (((f (#) |.E.|) | a) | V1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((f (#) |.E.|) | a) | V1)))) - (integral+ (M,(max- (((f (#) |.E.|) | a) | V1)))) is ext-real Element of ExtREAL
V2 is Element of X
((f (#) |.E.|) | a) . V2 is ext-real Element of ExtREAL
((b1 (#) |.E.|) | a) . V2 is ext-real Element of ExtREAL
(f (#) |.E.|) . V2 is ext-real Element of ExtREAL
f . V2 is ext-real Element of ExtREAL
|.E.| . V2 is ext-real Element of ExtREAL
(f . V2) * (|.E.| . V2) is ext-real Element of ExtREAL
E . V2 is ext-real Element of ExtREAL
|.(E . V2).| is ext-real Element of ExtREAL
(f . V2) * |.(E . V2).| is ext-real Element of ExtREAL
(b1 (#) |.E.|) . V2 is ext-real Element of ExtREAL
(R_EAL b1) * (|.E.| . V2) is ext-real Element of ExtREAL
(R_EAL b1) * |.(E . V2).| is ext-real Element of ExtREAL
((b1 (#) |.E.|) | a) - ((f (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((a1 (#) |.E.|) | a)) is ext-real Element of ExtREAL
max+ ((a1 (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((a1 (#) |.E.|) | a))) is ext-real Element of ExtREAL
max- ((a1 (#) |.E.|) | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((a1 (#) |.E.|) | a))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((a1 (#) |.E.|) | a)))) - (integral+ (M,(max- ((a1 (#) |.E.|) | a)))) is ext-real Element of ExtREAL
a1 (#) (|.E.| | a) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(a1 (#) (|.E.| | a))) is ext-real Element of ExtREAL
max+ (a1 (#) (|.E.| | a)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (a1 (#) (|.E.| | a)))) is ext-real Element of ExtREAL
max- (a1 (#) (|.E.| | a)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (a1 (#) (|.E.| | a)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (a1 (#) (|.E.| | a))))) - (integral+ (M,(max- (a1 (#) (|.E.| | a))))) is ext-real Element of ExtREAL
R_EAL a1 is ext-real Element of ExtREAL
(R_EAL a1) * (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
(dom ((b1 (#) |.E.|) | a)) /\ (dom ((f (#) |.E.|) | a)) is Element of K6(X)
V2 is Element of S
((f (#) |.E.|) | a) | V2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(((f (#) |.E.|) | a) | V2)) is ext-real Element of ExtREAL
max+ (((f (#) |.E.|) | a) | V2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (((f (#) |.E.|) | a) | V2))) is ext-real Element of ExtREAL
max- (((f (#) |.E.|) | a) | V2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (((f (#) |.E.|) | a) | V2))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((f (#) |.E.|) | a) | V2)))) - (integral+ (M,(max- (((f (#) |.E.|) | a) | V2)))) is ext-real Element of ExtREAL
((b1 (#) |.E.|) | a) | V2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(((b1 (#) |.E.|) | a) | V2)) is ext-real Element of ExtREAL
max+ (((b1 (#) |.E.|) | a) | V2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (((b1 (#) |.E.|) | a) | V2))) is ext-real Element of ExtREAL
max- (((b1 (#) |.E.|) | a) | V2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (((b1 (#) |.E.|) | a) | V2))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (((b1 (#) |.E.|) | a) | V2)))) - (integral+ (M,(max- (((b1 (#) |.E.|) | a) | V2)))) is ext-real Element of ExtREAL
(Integral (M,((f (#) |.E.|) | a))) / (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
y is V11() real ext-real Element of REAL
c1 is V11() real ext-real Element of REAL
y / c1 is V11() real ext-real Element of REAL
K39(c1) is V11() real ext-real set
K37(y,K39(c1)) is V11() real ext-real set
(Integral (M,(|.E.| | a))) / (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
c1 / c1 is V11() real ext-real Element of REAL
K37(c1,K39(c1)) is V11() real ext-real set
y * (c1 / c1) is V11() real ext-real Element of REAL
(Integral (M,((f (#) |.E.|) | a))) * ((Integral (M,(|.E.| | a))) / (Integral (M,(|.E.| | a)))) is ext-real Element of ExtREAL
(Integral (M,(|.E.| | a))) * ((Integral (M,((f (#) |.E.|) | a))) / (Integral (M,(|.E.| | a)))) is ext-real Element of ExtREAL
c1 * (y / c1) is V11() real ext-real Element of REAL
c is V11() real ext-real Element of REAL
R_EAL c is ext-real Element of ExtREAL
(R_EAL c) * (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
(sup b) * (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
b1 * c1 is V11() real ext-real Element of REAL
((sup b) * (Integral (M,(|.E.| | a)))) / (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
(b1 * c1) / c1 is V11() real ext-real Element of REAL
K37((b1 * c1),K39(c1)) is V11() real ext-real set
b1 * (c1 / c1) is V11() real ext-real Element of REAL
(sup b) * ((Integral (M,(|.E.| | a))) / (Integral (M,(|.E.| | a)))) is ext-real Element of ExtREAL
(inf b) * (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
a1 * c1 is V11() real ext-real Element of REAL
((inf b) * (Integral (M,(|.E.| | a)))) / (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
(a1 * c1) / c1 is V11() real ext-real Element of REAL
K37((a1 * c1),K39(c1)) is V11() real ext-real set
a1 * (c1 / c1) is V11() real ext-real Element of REAL
(inf b) * ((Integral (M,(|.E.| | a))) / (Integral (M,(|.E.| | a)))) is ext-real Element of ExtREAL
(sup b) * 1. is ext-real Element of ExtREAL
(inf b) * 1. is ext-real Element of ExtREAL
y is set
y is ext-real Element of ExtREAL
y is V11() real ext-real Element of REAL
R_EAL y is ext-real Element of ExtREAL
(R_EAL y) * (Integral (M,(|.E.| | a))) is ext-real Element of ExtREAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.S.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
M is set
|.S.| | M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
S | M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(S | M).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom (|.S.| | M) is Element of K6(X)
K6(X) is non empty set
dom |.S.| is Element of K6(X)
(dom |.S.|) /\ M is Element of K6(X)
dom S is Element of K6(X)
(dom S) /\ M is Element of K6(X)
dom (S | M) is Element of K6(X)
dom |.(S | M).| is Element of K6(X)
f is Element of X
|.(S | M).| . f is ext-real Element of ExtREAL
(S | M) . f is ext-real Element of ExtREAL
|.((S | M) . f).| is ext-real Element of ExtREAL
S . f is ext-real Element of ExtREAL
|.(S . f).| is ext-real Element of ExtREAL
(|.S.| | M) . f is ext-real Element of ExtREAL
|.S.| . f is ext-real Element of ExtREAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.S.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom S is Element of K6(X)
K6(X) is non empty set
dom |.S.| is Element of K6(X)
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.M.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
|.S.| + |.M.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (|.S.| + |.M.|) is Element of K6(X)
dom M is Element of K6(X)
(dom S) /\ (dom M) is Element of K6(X)
S + M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(S + M).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom |.(S + M).| is Element of K6(X)
rng |.S.| is V76() Element of K6(ExtREAL)
|.S.| " {-infty} is Element of K6(X)
rng |.M.| is V76() Element of K6(ExtREAL)
|.M.| " {-infty} is Element of K6(X)
dom |.M.| is Element of K6(X)
(dom |.S.|) /\ (dom |.M.|) is Element of K6(X)
|.M.| " {+infty} is Element of K6(X)
(|.S.| " {-infty}) /\ (|.M.| " {+infty}) is Element of K6(X)
|.S.| " {+infty} is Element of K6(X)
(|.S.| " {+infty}) /\ (|.M.| " {-infty}) is Element of K6(X)
((|.S.| " {-infty}) /\ (|.M.| " {+infty})) \/ ((|.S.| " {+infty}) /\ (|.M.| " {-infty})) is Element of K6(X)
((dom |.S.|) /\ (dom |.M.|)) \ (((|.S.| " {-infty}) /\ (|.M.| " {+infty})) \/ ((|.S.| " {+infty}) /\ (|.M.| " {-infty}))) is Element of K6(X)
(dom S) /\ (dom |.M.|) is Element of K6(X)
dom (S + M) is Element of K6(X)
S " {-infty} is Element of K6(X)
M " {+infty} is Element of K6(X)
(S " {-infty}) /\ (M " {+infty}) is Element of K6(X)
S " {+infty} is Element of K6(X)
M " {-infty} is Element of K6(X)
(S " {+infty}) /\ (M " {-infty}) is Element of K6(X)
((S " {-infty}) /\ (M " {+infty})) \/ ((S " {+infty}) /\ (M " {-infty})) is Element of K6(X)
((dom S) /\ (dom M)) \ (((S " {-infty}) /\ (M " {+infty})) \/ ((S " {+infty}) /\ (M " {-infty}))) is Element of K6(X)
(dom M) \ (((S " {-infty}) /\ (M " {+infty})) \/ ((S " {+infty}) /\ (M " {-infty}))) is Element of K6(X)
(dom S) /\ ((dom M) \ (((S " {-infty}) /\ (M " {+infty})) \/ ((S " {+infty}) /\ (M " {-infty})))) is Element of K6(X)
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.S.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
S + M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(S + M).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom |.(S + M).| is Element of K6(X)
K6(X) is non empty set
|.S.| | (dom |.(S + M).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.M.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
|.M.| | (dom |.(S + M).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(|.S.| | (dom |.(S + M).|)) + (|.M.| | (dom |.(S + M).|)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.S.| + |.M.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(|.S.| + |.M.|) | (dom |.(S + M).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
M | (dom |.(S + M).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(M | (dom |.(S + M).|)).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom |.M.| is Element of K6(X)
dom M is Element of K6(X)
dom (M | (dom |.(S + M).|)) is Element of K6(X)
(dom M) /\ (dom |.(S + M).|) is Element of K6(X)
dom |.(M | (dom |.(S + M).|)).| is Element of K6(X)
dom |.S.| is Element of K6(X)
dom S is Element of K6(X)
(dom |.(S + M).|) /\ (dom |.(S + M).|) is Element of K6(X)
(dom S) /\ (dom M) is Element of K6(X)
dom (|.S.| + |.M.|) is Element of K6(X)
dom ((|.S.| + |.M.|) | (dom |.(S + M).|)) is Element of K6(X)
S | (dom |.(S + M).|) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (S | (dom |.(S + M).|)) is Element of K6(X)
(dom S) /\ (dom |.(S + M).|) is Element of K6(X)
|.(S | (dom |.(S + M).|)).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom ((|.S.| | (dom |.(S + M).|)) + (|.M.| | (dom |.(S + M).|))) is Element of K6(X)
(dom (S | (dom |.(S + M).|))) /\ (dom (M | (dom |.(S + M).|))) is Element of K6(X)
dom |.(S | (dom |.(S + M).|)).| is Element of K6(X)
f is Element of X
((|.S.| + |.M.|) | (dom |.(S + M).|)) . f is ext-real Element of ExtREAL
(|.S.| + |.M.|) . f is ext-real Element of ExtREAL
|.S.| . f is ext-real Element of ExtREAL
|.M.| . f is ext-real Element of ExtREAL
(|.S.| . f) + (|.M.| . f) is ext-real Element of ExtREAL
S . f is ext-real Element of ExtREAL
|.(S . f).| is ext-real Element of ExtREAL
|.(S . f).| + (|.M.| . f) is ext-real Element of ExtREAL
((|.S.| | (dom |.(S + M).|)) + (|.M.| | (dom |.(S + M).|))) . f is ext-real Element of ExtREAL
(|.S.| | (dom |.(S + M).|)) . f is ext-real Element of ExtREAL
(|.M.| | (dom |.(S + M).|)) . f is ext-real Element of ExtREAL
((|.S.| | (dom |.(S + M).|)) . f) + ((|.M.| | (dom |.(S + M).|)) . f) is ext-real Element of ExtREAL
(S | (dom |.(S + M).|)) . f is ext-real Element of ExtREAL
|.((S | (dom |.(S + M).|)) . f).| is ext-real Element of ExtREAL
|.(M | (dom |.(S + M).|)).| . f is ext-real Element of ExtREAL
|.((S | (dom |.(S + M).|)) . f).| + (|.(M | (dom |.(S + M).|)).| . f) is ext-real Element of ExtREAL
(M | (dom |.(S + M).|)) . f is ext-real Element of ExtREAL
|.((M | (dom |.(S + M).|)) . f).| is ext-real Element of ExtREAL
|.((S | (dom |.(S + M).|)) . f).| + |.((M | (dom |.(S + M).|)) . f).| is ext-real Element of ExtREAL
|.(S . f).| + |.((M | (dom |.(S + M).|)) . f).| is ext-real Element of ExtREAL
M . f is ext-real Element of ExtREAL
|.(M . f).| is ext-real Element of ExtREAL
|.(S . f).| + |.(M . f).| is ext-real Element of ExtREAL
X is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.S.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
S + M is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.(S + M).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom |.(S + M).| is Element of K6(X)
K6(X) is non empty set
|.M.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
|.S.| + |.M.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
f is set
|.(S + M).| . f is ext-real Element of ExtREAL
(|.S.| + |.M.|) . f is ext-real Element of ExtREAL
S . f is ext-real Element of ExtREAL
M . f is ext-real Element of ExtREAL
(S . f) + (M . f) is ext-real Element of ExtREAL
|.((S . f) + (M . f)).| is ext-real Element of ExtREAL
|.(S . f).| is ext-real Element of ExtREAL
|.(M . f).| is ext-real Element of ExtREAL
|.(S . f).| + |.(M . f).| is ext-real Element of ExtREAL
dom (S + M) is Element of K6(X)
(S + M) . f is ext-real Element of ExtREAL
|.((S + M) . f).| is ext-real Element of ExtREAL
dom |.M.| is Element of K6(X)
|.M.| . f is ext-real Element of ExtREAL
dom M is Element of K6(X)
dom |.S.| is Element of K6(X)
dom S is Element of K6(X)
(dom S) /\ (dom M) is Element of K6(X)
dom (|.S.| + |.M.|) is Element of K6(X)
|.S.| . f is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.f.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
f + E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (f + E) is Element of K6(X)
|.(f + E).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
|.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued nonnegative Element of K6(K7(X,ExtREAL))
dom E is Element of K6(X)
a is Element of S
a is Element of S
dom |.(f + E).| is Element of K6(X)
|.f.| + |.E.| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
a is Element of X
|.(f + E).| . a is ext-real Element of ExtREAL
(|.f.| + |.E.|) . a is ext-real Element of ExtREAL
(|.f.| + |.E.|) - |.(f + E).| is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
(dom f) /\ (dom E) is Element of K6(X)
f " {-infty} is Element of K6(X)
E " {+infty} is Element of K6(X)
(f " {-infty}) /\ (E " {+infty}) is Element of K6(X)
f " {+infty} is Element of K6(X)
E " {-infty} is Element of K6(X)
(f " {+infty}) /\ (E " {-infty}) is Element of K6(X)
((f " {-infty}) /\ (E " {+infty})) \/ ((f " {+infty}) /\ (E " {-infty})) is Element of K6(X)
((dom f) /\ (dom E)) \ (((f " {-infty}) /\ (E " {+infty})) \/ ((f " {+infty}) /\ (E " {-infty}))) is Element of K6(X)
a1 is Element of S
dom (|.f.| + |.E.|) is Element of K6(X)
(dom (|.f.| + |.E.|)) /\ (dom |.(f + E).|) is Element of K6(X)
a1 is Element of S
|.(f + E).| | a1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(|.(f + E).| | a1)) is ext-real Element of ExtREAL
max+ (|.(f + E).| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (|.(f + E).| | a1))) is ext-real Element of ExtREAL
max- (|.(f + E).| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (|.(f + E).| | a1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (|.(f + E).| | a1)))) - (integral+ (M,(max- (|.(f + E).| | a1)))) is ext-real Element of ExtREAL
(|.f.| + |.E.|) | a1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((|.f.| + |.E.|) | a1)) is ext-real Element of ExtREAL
max+ ((|.f.| + |.E.|) | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((|.f.| + |.E.|) | a1))) is ext-real Element of ExtREAL
max- ((|.f.| + |.E.|) | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((|.f.| + |.E.|) | a1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((|.f.| + |.E.|) | a1)))) - (integral+ (M,(max- ((|.f.| + |.E.|) | a1)))) is ext-real Element of ExtREAL
|.E.| | a1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
|.f.| | a1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (|.f.| | a1) is Element of K6(X)
dom (|.E.| | a1) is Element of K6(X)
(dom (|.f.| | a1)) /\ (dom (|.E.| | a1)) is Element of K6(X)
(|.f.| | a1) + (|.E.| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((|.f.| | a1) + (|.E.| | a1))) is ext-real Element of ExtREAL
max+ ((|.f.| | a1) + (|.E.| | a1)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((|.f.| | a1) + (|.E.| | a1)))) is ext-real Element of ExtREAL
max- ((|.f.| | a1) + (|.E.| | a1)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((|.f.| | a1) + (|.E.| | a1)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((|.f.| | a1) + (|.E.| | a1))))) - (integral+ (M,(max- ((|.f.| | a1) + (|.E.| | a1))))) is ext-real Element of ExtREAL
b1 is Element of S
(|.f.| | a1) | b1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((|.f.| | a1) | b1)) is ext-real Element of ExtREAL
max+ ((|.f.| | a1) | b1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((|.f.| | a1) | b1))) is ext-real Element of ExtREAL
max- ((|.f.| | a1) | b1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((|.f.| | a1) | b1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((|.f.| | a1) | b1)))) - (integral+ (M,(max- ((|.f.| | a1) | b1)))) is ext-real Element of ExtREAL
(|.E.| | a1) | b1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((|.E.| | a1) | b1)) is ext-real Element of ExtREAL
max+ ((|.E.| | a1) | b1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((|.E.| | a1) | b1))) is ext-real Element of ExtREAL
max- ((|.E.| | a1) | b1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((|.E.| | a1) | b1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((|.E.| | a1) | b1)))) - (integral+ (M,(max- ((|.E.| | a1) | b1)))) is ext-real Element of ExtREAL
(Integral (M,((|.f.| | a1) | b1))) + (Integral (M,((|.E.| | a1) | b1))) is ext-real Element of ExtREAL
Integral (M,(|.f.| | a1)) is ext-real Element of ExtREAL
max+ (|.f.| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (|.f.| | a1))) is ext-real Element of ExtREAL
max- (|.f.| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (|.f.| | a1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (|.f.| | a1)))) - (integral+ (M,(max- (|.f.| | a1)))) is ext-real Element of ExtREAL
Integral (M,(|.E.| | a1)) is ext-real Element of ExtREAL
max+ (|.E.| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (|.E.| | a1))) is ext-real Element of ExtREAL
max- (|.E.| | a1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (|.E.| | a1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (|.E.| | a1)))) - (integral+ (M,(max- (|.E.| | a1)))) is ext-real Element of ExtREAL
(Integral (M,(|.f.| | a1))) + (Integral (M,(|.E.| | a1))) is ext-real Element of ExtREAL
dom |.E.| is Element of K6(X)
(dom |.E.|) /\ a1 is Element of K6(X)
(dom E) /\ a1 is Element of K6(X)
dom |.f.| is Element of K6(X)
(dom |.f.|) /\ a1 is Element of K6(X)
(dom f) /\ a1 is Element of K6(X)
((dom f) /\ a1) /\ a1 is Element of K6(X)
(((dom f) /\ a1) /\ a1) /\ (dom E) is Element of K6(X)
a1 /\ a1 is M9(X,S)
(dom f) /\ (a1 /\ a1) is Element of K6(X)
((dom f) /\ (a1 /\ a1)) /\ (dom E) is Element of K6(X)
((dom f) /\ (dom E)) /\ a1 is Element of K6(X)
X is non empty set
S is set
chi (S,X) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
max+ (chi (S,X)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (max+ (chi (S,X))) is Element of K6(X)
K6(X) is non empty set
dom (chi (S,X)) is Element of K6(X)
rng (chi (S,X)) is V76() Element of K6(ExtREAL)
{0,1} is non empty V75() V76() V77() V78() V79() V80() set
M is Element of X
(max+ (chi (S,X))) . M is ext-real Element of ExtREAL
(chi (S,X)) . M is ext-real Element of ExtREAL
max (((chi (S,X)) . M),0.) is ext-real set
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Element of S
M . f is ext-real Element of ExtREAL
chi (f,X) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
Integral (M,(chi (f,X))) is ext-real Element of ExtREAL
max+ (chi (f,X)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (chi (f,X)))) is ext-real Element of ExtREAL
max- (chi (f,X)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (chi (f,X)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (chi (f,X))))) - (integral+ (M,(max- (chi (f,X))))) is ext-real Element of ExtREAL
(chi (f,X)) | f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((chi (f,X)) | f)) is ext-real Element of ExtREAL
max+ ((chi (f,X)) | f) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((chi (f,X)) | f))) is ext-real Element of ExtREAL
max- ((chi (f,X)) | f) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((chi (f,X)) | f))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((chi (f,X)) | f)))) - (integral+ (M,(max- ((chi (f,X)) | f)))) is ext-real Element of ExtREAL
E is Element of S
E \ f is M9(X,S)
b is Element of X
(chi (f,X)) . b is ext-real Element of ExtREAL
- ((chi (f,X)) . b) is ext-real Element of ExtREAL
max ((- ((chi (f,X)) . b)),0.) is ext-real set
dom (max- (chi (f,X))) is Element of K6(X)
(max- (chi (f,X))) . b is ext-real Element of ExtREAL
dom (chi (f,X)) is Element of K6(X)
dom (max+ (chi (f,X))) is Element of K6(X)
E /\ (E \ f) is M9(X,S)
(max+ (chi (f,X))) | (E \ f) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((max+ (chi (f,X))) | (E \ f)) is Element of K6(X)
b is Element of X
(chi (f,X)) . b is ext-real Element of ExtREAL
(max+ (chi (f,X))) . b is ext-real Element of ExtREAL
((max+ (chi (f,X))) | (E \ f)) . b is ext-real Element of ExtREAL
integral+ (M,((max+ (chi (f,X))) | (E \ f))) is ext-real Element of ExtREAL
E /\ f is M9(X,S)
(max+ (chi (f,X))) | f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((max+ (chi (f,X))) | f) is Element of K6(X)
f \/ (E \ f) is M9(X,S)
(max+ (chi (f,X))) | (f \/ (E \ f)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
b is set
(max+ (chi (f,X))) . b is ext-real Element of ExtREAL
integral+ (M,((max+ (chi (f,X))) | (f \/ (E \ f)))) is ext-real Element of ExtREAL
integral+ (M,((max+ (chi (f,X))) | f)) is ext-real Element of ExtREAL
(integral+ (M,((max+ (chi (f,X))) | f))) + (integral+ (M,((max+ (chi (f,X))) | (E \ f)))) is ext-real Element of ExtREAL
b is set
(chi (f,X)) . b is ext-real Element of ExtREAL
(max+ (chi (f,X))) . b is ext-real Element of ExtREAL
((max+ (chi (f,X))) | f) . b is ext-real Element of ExtREAL
integral' (M,((max+ (chi (f,X))) | f)) is ext-real Element of ExtREAL
R_EAL 1 is ext-real Element of ExtREAL
M . (dom ((max+ (chi (f,X))) | f)) is ext-real Element of ExtREAL
(R_EAL 1) * (M . (dom ((max+ (chi (f,X))) | f))) is ext-real Element of ExtREAL
dom ((chi (f,X)) | f) is Element of K6(X)
integral+ (M,((chi (f,X)) | f)) is ext-real Element of ExtREAL
(R_EAL 1) * (M . f) is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Element of S
chi (f,X) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
E is Element of S
f /\ E is M9(X,S)
M . (f /\ E) is ext-real Element of ExtREAL
(chi (f,X)) | E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((chi (f,X)) | E)) is ext-real Element of ExtREAL
max+ ((chi (f,X)) | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((chi (f,X)) | E))) is ext-real Element of ExtREAL
max- ((chi (f,X)) | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((chi (f,X)) | E))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((chi (f,X)) | E)))) - (integral+ (M,(max- ((chi (f,X)) | E)))) is ext-real Element of ExtREAL
E \ f is M9(X,S)
(f /\ E) \/ (E \ f) is M9(X,S)
(chi (f,X)) | (f /\ E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((chi (f,X)) | (f /\ E)) is Element of K6(X)
dom (chi (f,X)) is Element of K6(X)
(dom (chi (f,X))) /\ (f /\ E) is Element of K6(X)
X /\ (f /\ E) is Element of K6(X)
chi ((f /\ E),X) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(chi ((f /\ E),X)) | (f /\ E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((chi ((f /\ E),X)) | (f /\ E)) is Element of K6(X)
dom (chi ((f /\ E),X)) is Element of K6(X)
(dom (chi ((f /\ E),X))) /\ (f /\ E) is Element of K6(X)
a1 is Element of X
((chi ((f /\ E),X)) | (f /\ E)) . a1 is ext-real Element of ExtREAL
(chi ((f /\ E),X)) . a1 is ext-real Element of ExtREAL
((chi (f,X)) | (f /\ E)) . a1 is ext-real Element of ExtREAL
(chi (f,X)) . a1 is ext-real Element of ExtREAL
Integral (M,((chi (f,X)) | (f /\ E))) is ext-real Element of ExtREAL
max+ ((chi (f,X)) | (f /\ E)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((chi (f,X)) | (f /\ E)))) is ext-real Element of ExtREAL
max- ((chi (f,X)) | (f /\ E)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((chi (f,X)) | (f /\ E)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((chi (f,X)) | (f /\ E))))) - (integral+ (M,(max- ((chi (f,X)) | (f /\ E))))) is ext-real Element of ExtREAL
a is Element of S
(chi (f,X)) | (E \ f) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom ((chi (f,X)) | (E \ f)) is Element of K6(X)
(dom (chi (f,X))) /\ (E \ f) is Element of K6(X)
a1 is set
(chi (f,X)) . a1 is ext-real Element of ExtREAL
rng (chi (f,X)) is V76() Element of K6(ExtREAL)
{0,1} is non empty V75() V76() V77() V78() V79() V80() set
a1 is Element of X
X \ f is Element of K6(X)
(chi (f,X)) . a1 is ext-real Element of ExtREAL
((chi (f,X)) | (E \ f)) . a1 is ext-real Element of ExtREAL
integral+ (M,((chi (f,X)) | (E \ f))) is ext-real Element of ExtREAL
Integral (M,((chi (f,X)) | (E \ f))) is ext-real Element of ExtREAL
max+ ((chi (f,X)) | (E \ f)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((chi (f,X)) | (E \ f)))) is ext-real Element of ExtREAL
max- ((chi (f,X)) | (E \ f)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((chi (f,X)) | (E \ f)))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((chi (f,X)) | (E \ f))))) - (integral+ (M,(max- ((chi (f,X)) | (E \ f))))) is ext-real Element of ExtREAL
(Integral (M,((chi (f,X)) | (f /\ E)))) + (Integral (M,((chi (f,X)) | (E \ f)))) is ext-real Element of ExtREAL
X is non empty set
K6(X) is non empty set
K6(K6(X)) is non empty set
K7(X,ExtREAL) is non empty ext-real-valued set
K6(K7(X,ExtREAL)) is non empty set
S is non empty V30() V31() V32() compl-closed sigma-multiplicative sigma-additive Element of K6(K6(X))
K7(S,ExtREAL) is non empty ext-real-valued set
K6(K7(S,ExtREAL)) is non empty set
M is Relation-like S -defined ExtREAL -valued V18() V27(S, ExtREAL ) ext-real-valued zeroed nonnegative sigma-additive Element of K6(K7(S,ExtREAL))
f is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom f is Element of K6(X)
E is Element of S
M . E is ext-real Element of ExtREAL
f | E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,(f | E)) is ext-real Element of ExtREAL
max+ (f | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ (f | E))) is ext-real Element of ExtREAL
max- (f | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- (f | E))) is ext-real Element of ExtREAL
(integral+ (M,(max+ (f | E)))) - (integral+ (M,(max- (f | E)))) is ext-real Element of ExtREAL
a is V11() real ext-real set
R_EAL a is ext-real Element of ExtREAL
(R_EAL a) * (M . E) is ext-real Element of ExtREAL
b is V11() real ext-real set
R_EAL b is ext-real Element of ExtREAL
(R_EAL b) * (M . E) is ext-real Element of ExtREAL
chi (E,X) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(chi (E,X)) | E is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
a1 is V11() real ext-real Element of REAL
a1 (#) ((chi (E,X)) | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (a1 (#) ((chi (E,X)) | E)) is Element of K6(X)
E1 is Element of X
(a1 (#) ((chi (E,X)) | E)) . E1 is ext-real Element of ExtREAL
(f | E) . E1 is ext-real Element of ExtREAL
dom ((chi (E,X)) | E) is Element of K6(X)
dom (chi (E,X)) is Element of K6(X)
(dom (chi (E,X))) /\ E is Element of K6(X)
f . E1 is ext-real Element of ExtREAL
((chi (E,X)) | E) . E1 is ext-real Element of ExtREAL
(R_EAL a) * (((chi (E,X)) | E) . E1) is ext-real Element of ExtREAL
(chi (E,X)) . E1 is ext-real Element of ExtREAL
(R_EAL a) * ((chi (E,X)) . E1) is ext-real Element of ExtREAL
(R_EAL a) * 1. is ext-real Element of ExtREAL
(f | E) - (a1 (#) ((chi (E,X)) | E)) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (f | E) is Element of K6(X)
(dom (f | E)) /\ (dom (a1 (#) ((chi (E,X)) | E))) is Element of K6(X)
E1 is Element of S
(a1 (#) ((chi (E,X)) | E)) | E1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((a1 (#) ((chi (E,X)) | E)) | E1)) is ext-real Element of ExtREAL
max+ ((a1 (#) ((chi (E,X)) | E)) | E1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((a1 (#) ((chi (E,X)) | E)) | E1))) is ext-real Element of ExtREAL
max- ((a1 (#) ((chi (E,X)) | E)) | E1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((a1 (#) ((chi (E,X)) | E)) | E1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((a1 (#) ((chi (E,X)) | E)) | E1)))) - (integral+ (M,(max- ((a1 (#) ((chi (E,X)) | E)) | E1)))) is ext-real Element of ExtREAL
(f | E) | E1 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((f | E) | E1)) is ext-real Element of ExtREAL
max+ ((f | E) | E1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((f | E) | E1))) is ext-real Element of ExtREAL
max- ((f | E) | E1) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((f | E) | E1))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((f | E) | E1)))) - (integral+ (M,(max- ((f | E) | E1)))) is ext-real Element of ExtREAL
(dom f) /\ E is Element of K6(X)
dom ((chi (E,X)) | E) is Element of K6(X)
dom (chi (E,X)) is Element of K6(X)
(dom (chi (E,X))) /\ E is Element of K6(X)
X /\ E is Element of K6(X)
b1 is V11() real ext-real Element of REAL
b1 (#) ((chi (E,X)) | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
dom (b1 (#) ((chi (E,X)) | E)) is Element of K6(X)
E2 is Element of X
(f | E) . E2 is ext-real Element of ExtREAL
(b1 (#) ((chi (E,X)) | E)) . E2 is ext-real Element of ExtREAL
f . E2 is ext-real Element of ExtREAL
((chi (E,X)) | E) . E2 is ext-real Element of ExtREAL
(R_EAL b) * (((chi (E,X)) | E) . E2) is ext-real Element of ExtREAL
(chi (E,X)) . E2 is ext-real Element of ExtREAL
(R_EAL b) * ((chi (E,X)) . E2) is ext-real Element of ExtREAL
(R_EAL b) * 1. is ext-real Element of ExtREAL
(b1 (#) ((chi (E,X)) | E)) - (f | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
(dom (f | E)) /\ (dom (b1 (#) ((chi (E,X)) | E))) is Element of K6(X)
E2 is Element of S
(f | E) | E2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((f | E) | E2)) is ext-real Element of ExtREAL
max+ ((f | E) | E2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((f | E) | E2))) is ext-real Element of ExtREAL
max- ((f | E) | E2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((f | E) | E2))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((f | E) | E2)))) - (integral+ (M,(max- ((f | E) | E2)))) is ext-real Element of ExtREAL
(b1 (#) ((chi (E,X)) | E)) | E2 is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
Integral (M,((b1 (#) ((chi (E,X)) | E)) | E2)) is ext-real Element of ExtREAL
max+ ((b1 (#) ((chi (E,X)) | E)) | E2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((b1 (#) ((chi (E,X)) | E)) | E2))) is ext-real Element of ExtREAL
max- ((b1 (#) ((chi (E,X)) | E)) | E2) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((b1 (#) ((chi (E,X)) | E)) | E2))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((b1 (#) ((chi (E,X)) | E)) | E2)))) - (integral+ (M,(max- ((b1 (#) ((chi (E,X)) | E)) | E2)))) is ext-real Element of ExtREAL
E /\ E is M9(X,S)
Integral (M,((chi (E,X)) | E)) is ext-real Element of ExtREAL
max+ ((chi (E,X)) | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max+ ((chi (E,X)) | E))) is ext-real Element of ExtREAL
max- ((chi (E,X)) | E) is Relation-like X -defined ExtREAL -valued V18() ext-real-valued Element of K6(K7(X,ExtREAL))
integral+ (M,(max- ((chi (E,X)) | E))) is ext-real Element of ExtREAL
(integral+ (M,(max+ ((chi (E,X)) | E)))) - (integral+ (M,(max- ((chi (E,X)) | E)))) is ext-real Element of ExtREAL