let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is E -measurable & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
let S be SigmaField of X; for M being sigma_Measure of S
for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is E -measurable & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
let M be sigma_Measure of S; for f, g being PartFunc of X,ExtREAL
for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is E -measurable & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
let f, g be PartFunc of X,ExtREAL; for E being Element of S
for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is E -measurable & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
let E be Element of S; for F being non empty Subset of ExtREAL st (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is E -measurable & rng f is real-bounded & g is_integrable_on M holds
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
let F be non empty Subset of ExtREAL; ( (dom f) /\ (dom g) = E & rng f = F & g is V71() & f is E -measurable & rng f is real-bounded & g is_integrable_on M implies ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) ) )
assume that
A1:
(dom f) /\ (dom g) = E
and
A2:
rng f = F
and
A3:
g is V71()
and
A4:
f is E -measurable
and
A5:
rng f is real-bounded
and
A6:
g is_integrable_on M
; ( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
A7:
dom ((f (#) |.g.|) | E) = (dom (f (#) |.g.|)) /\ E
by RELAT_1:61;
A8:
rng f is Subset of REAL
by A5, Th16, MESFUNC2:32;
then
not +infty in rng f
;
then A9:
rng f <> {+infty}
by TARSKI:def 1;
A10:
rng f is bounded_above
by A5, XXREAL_2:def 11;
not -infty in rng f
by A8;
then A11:
rng f <> {-infty}
by TARSKI:def 1;
rng f is bounded_below
by A5, XXREAL_2:def 11;
then reconsider k0 = inf F, l0 = sup F as Element of REAL by A2, A10, A9, A11, XXREAL_2:57, XXREAL_2:58;
A12:
|.(sup F).| = |.l0.|
by EXTREAL1:12;
|.(inf F).| = |.k0.|
by EXTREAL1:12;
then reconsider k1 = |.(inf F).|, l1 = |.(sup F).| as Real by A12;
A13:
E c= dom f
by A1, XBOOLE_1:17;
A14:
sup F is UpperBound of rng f
by A2, XXREAL_2:def 3;
A15:
E c= dom g
by A1, XBOOLE_1:17;
then A16:
E c= dom |.g.|
by MESFUNC1:def 10;
A17:
dom |.g.| = dom g
by MESFUNC1:def 10;
for x being Element of X st x in dom |.g.| holds
|.(|.g.| . x).| < +infty
then A19:
|.g.| is V71()
by MESFUNC2:def 1;
A20:
f is V71()
by A5, Th16;
consider E1 being Element of S such that
A21:
E1 = dom g
and
A22:
g is E1 -measurable
by A6;
A23:
E1 = dom |.g.|
by A21, MESFUNC1:def 10;
|.g.| is E1 -measurable
by A21, A22, MESFUNC2:27;
then A24:
|.g.| is E -measurable
by A1, A21, MESFUNC1:30, XBOOLE_1:17;
(dom f) /\ (dom |.g.|) = E
by A1, MESFUNC1:def 10;
then A25:
f (#) |.g.| is E -measurable
by A4, A24, A20, A19, Th15;
A26:
|.g.| is_integrable_on M
by A6, MESFUNC5:100;
then A27:
|.g.| | E is_integrable_on M
by MESFUNC5:97;
A28:
dom (f (#) |.g.|) = (dom f) /\ (dom |.g.|)
by MESFUNC1:def 5;
then A29:
dom (f (#) |.g.|) = E
by A1, MESFUNC1:def 10;
A30:
dom (k0 (#) |.g.|) = dom |.g.|
by MESFUNC1:def 6;
then A31:
dom ((k0 (#) |.g.|) | E) = E
by A16, RELAT_1:62;
A32:
inf F is LowerBound of rng f
by A2, XXREAL_2:def 4;
A33:
for x being Element of X st x in E holds
( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| )
for x being Element of X st x in dom ((k0 (#) |.g.|) | E) holds
((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x
proof
let x be
Element of
X;
( x in dom ((k0 (#) |.g.|) | E) implies ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x )
assume A37:
x in dom ((k0 (#) |.g.|) | E)
;
((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x
then A38:
((k0 (#) |.g.|) | E) . x = (k0 (#) |.g.|) . x
by FUNCT_1:47;
(f (#) |.g.|) . x = (f . x) * (|.g.| . x)
by A29, A31, A37, MESFUNC1:def 5;
then A39:
(f (#) |.g.|) . x = (f . x) * |.(g . x).|
by A16, A31, A37, MESFUNC1:def 10;
(k0 (#) |.g.|) . x = k0 * (|.g.| . x)
by A16, A30, A31, A37, MESFUNC1:def 6;
then
(k0 (#) |.g.|) . x = k0 * |.(g . x).|
by A16, A31, A37, MESFUNC1:def 10;
then
(k0 (#) |.g.|) . x <= (f (#) |.g.|) . x
by A33, A31, A37, A39;
hence
((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x
by A29, A7, A31, A37, A38, FUNCT_1:47;
verum
end;
then A40:
((f (#) |.g.|) | E) - ((k0 (#) |.g.|) | E) is nonnegative
by Th1;
A41:
dom (l0 (#) |.g.|) = dom |.g.|
by MESFUNC1:def 6;
then A42:
dom ((l0 (#) |.g.|) | E) = E
by A16, RELAT_1:62;
A43:
dom (f (#) g) = E
by A1, MESFUNC1:def 5;
then A44:
dom ((f (#) g) | E) = E
by RELAT_1:62;
then A45:
dom |.((f (#) g) | E).| = E
by MESFUNC1:def 10;
A46:
for x being Element of X st x in dom ((f (#) |.g.|) | E) holds
|.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x
proof
let x be
Element of
X;
( x in dom ((f (#) |.g.|) | E) implies |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x )
assume A47:
x in dom ((f (#) |.g.|) | E)
;
|.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x
then A48:
((f (#) |.g.|) | E) . x = (f (#) |.g.|) . x
by FUNCT_1:47;
|.((f (#) |.g.|) . x).| =
|.((f . x) * (|.g.| . x)).|
by A29, A7, A47, MESFUNC1:def 5
.=
|.((f . x) * |.(g . x).|).|
by A1, A17, A15, A28, A7, A47, MESFUNC1:def 10
.=
|.(f . x).| * |.|.(g . x).|.|
by EXTREAL1:19
.=
|.(f . x).| * |.(g . x).|
;
then A49:
|.((f (#) |.g.|) . x).| = |.((f . x) * (g . x)).|
by EXTREAL1:19;
dom |.(f (#) g).| = E
by A43, MESFUNC1:def 10;
then A50:
|.(f (#) g).| . x = |.((f (#) g) . x).|
by A29, A7, A47, MESFUNC1:def 10;
|.(((f (#) g) | E) . x).| = |.((f (#) g) . x).|
by A44, A29, A7, A47, FUNCT_1:47;
then
|.((f (#) g) | E).| . x = |.(f (#) g).| . x
by A45, A29, A7, A47, A50, MESFUNC1:def 10;
hence
|.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x
by A43, A29, A7, A47, A49, A50, A48, MESFUNC1:def 5;
verum
end;
Integral (M,((l0 (#) |.g.|) | E)) = Integral (M,(l0 (#) (|.g.| | E)))
by Th2;
then A51:
Integral (M,((l0 (#) |.g.|) | E)) = l0 * (Integral (M,(|.g.| | E)))
by A27, MESFUNC5:110;
A52:
(dom (f (#) g)) /\ E = E
by A43;
g is E -measurable
by A1, A21, A22, MESFUNC1:30, XBOOLE_1:17;
then
f (#) g is E -measurable
by A1, A3, A4, A20, Th15;
then A53:
(f (#) g) | E is E -measurable
by A52, MESFUNC5:42;
A54:
for x being Element of X st x in E holds
|.(f . x).| <= |.(inf F).| + |.(sup F).|
proof
0 <= |.k0.|
by COMPLEX1:46;
then A55:
l0 + 0 <= l0 + |.k0.|
by XREAL_1:6;
l0 <= |.l0.|
by COMPLEX1:76;
then
l0 + |.k0.| <= |.l0.| + |.k0.|
by XREAL_1:6;
then A56:
l0 <= |.l0.| + |.k0.|
by A55, XXREAL_0:2;
0 <= |.l0.|
by COMPLEX1:46;
then A57:
(- |.k0.|) - |.l0.| <= (- |.k0.|) - 0
by XREAL_1:10;
- |.k0.| <= k0
by COMPLEX1:76;
then A58:
(- |.k0.|) - |.l0.| <= k0
by A57, XXREAL_0:2;
let x be
Element of
X;
( x in E implies |.(f . x).| <= |.(inf F).| + |.(sup F).| )
A59:
|.k0.| = |.(inf F).|
by EXTREAL1:12;
assume A60:
x in E
;
|.(f . x).| <= |.(inf F).| + |.(sup F).|
then
f . x in rng f
by A13, FUNCT_1:3;
then reconsider fx =
f . x as
Real by A8;
A61:
|.l0.| = |.(sup F).|
by EXTREAL1:12;
fx <= l0
by A13, A14, A60, FUNCT_1:3, XXREAL_2:def 1;
then A62:
fx <= |.k0.| + |.l0.|
by A56, XXREAL_0:2;
k0 <= fx
by A13, A32, A60, FUNCT_1:3, XXREAL_2:def 2;
then
- (|.k0.| + |.l0.|) <= fx
by A58, XXREAL_0:2;
then A63:
|.fx.| <= |.k0.| + |.l0.|
by A62, ABSVALUE:5;
|.fx.| = |.(f . x).|
by EXTREAL1:12;
hence
|.(f . x).| <= |.(inf F).| + |.(sup F).|
by A63, A59, A61, SUPINF_2:1;
verum
end;
dom (((k1 + l1) (#) |.g.|) | E) = dom ((k1 + l1) (#) (|.g.| | E))
by Th2;
then
dom (((k1 + l1) (#) |.g.|) | E) = dom (|.g.| | E)
by MESFUNC1:def 6;
then A64:
dom (((k1 + l1) (#) |.g.|) | E) = E
by A16, RELAT_1:62;
A65:
dom ((k1 + l1) (#) |.g.|) = dom |.g.|
by MESFUNC1:def 6;
A66:
for x being Element of X st x in dom ((f (#) g) | E) holds
|.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x
proof
let x be
Element of
X;
( x in dom ((f (#) g) | E) implies |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x )
assume A67:
x in dom ((f (#) g) | E)
;
|.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x
then A68:
((f (#) g) | E) . x = (f (#) g) . x
by FUNCT_1:47;
dom (f | E) = E
by A1, RELAT_1:62, XBOOLE_1:17;
then A69:
(f | E) . x = f . x
by A44, A67, FUNCT_1:47;
dom (g | E) = E
by A1, RELAT_1:62, XBOOLE_1:17;
then A70:
(g | E) . x = g . x
by A44, A67, FUNCT_1:47;
0 <= |.((g | E) . x).|
by EXTREAL1:14;
then A71:
|.((f | E) . x).| * |.((g | E) . x).| <= (|.(inf F).| + |.(sup F).|) * |.((g | E) . x).|
by A44, A54, A67, A69, XXREAL_3:71;
A72:
(((k1 + l1) (#) |.g.|) | E) . x = ((k1 + l1) (#) |.g.|) . x
by A44, A64, A67, FUNCT_1:47;
|.((f (#) g) . x).| = |.((f . x) * (g . x)).|
by A43, A44, A67, MESFUNC1:def 5;
then A73:
|.(((f (#) g) | E) . x).| = |.((f | E) . x).| * |.((g | E) . x).|
by A68, A69, A70, EXTREAL1:19;
((k1 + l1) (#) |.g.|) . x = (k1 + l1) * (|.g.| . x)
by A16, A44, A65, A67, MESFUNC1:def 6;
then
(((k1 + l1) (#) |.g.|) | E) . x = (k1 + l1) * |.((g | E) . x).|
by A16, A44, A67, A70, A72, MESFUNC1:def 10;
hence
|.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x
by A71, A73, SUPINF_2:1;
verum
end;
(k1 + l1) (#) |.g.| is_integrable_on M
by A26, MESFUNC5:110;
then A74:
((k1 + l1) (#) |.g.|) | E is_integrable_on M
by MESFUNC5:97;
then
(f (#) g) | E is_integrable_on M
by A44, A64, A53, A66, MESFUNC5:102;
then A75:
|.((f (#) g) | E).| is_integrable_on M
by MESFUNC5:100;
(dom (f (#) |.g.|)) /\ E = E
by A29;
then
(f (#) |.g.|) | E is E -measurable
by A25, MESFUNC5:42;
then A76:
(f (#) |.g.|) | E is_integrable_on M
by A45, A29, A7, A75, A46, MESFUNC5:102;
then A77:
-infty < Integral (M,((f (#) |.g.|) | E))
by MESFUNC5:96;
k0 (#) |.g.| is_integrable_on M
by A26, MESFUNC5:110;
then
(k0 (#) |.g.|) | E is_integrable_on M
by MESFUNC5:97;
then consider V1 being Element of S such that
A78:
V1 = (dom ((k0 (#) |.g.|) | E)) /\ (dom ((f (#) |.g.|) | E))
and
A79:
Integral (M,(((k0 (#) |.g.|) | E) | V1)) <= Integral (M,(((f (#) |.g.|) | E) | V1))
by A76, A40, Th3;
A80:
((f (#) |.g.|) | E) | V1 = (f (#) |.g.|) | E
by A29, A7, A31, A78, RELAT_1:68;
A81:
dom (f (#) |.g.|) c= dom (l0 (#) |.g.|)
by A28, A41, XBOOLE_1:17;
for x being Element of X st x in dom ((f (#) |.g.|) | E) holds
((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x
proof
let x be
Element of
X;
( x in dom ((f (#) |.g.|) | E) implies ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x )
assume A82:
x in dom ((f (#) |.g.|) | E)
;
((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x
then A83:
((f (#) |.g.|) | E) . x = (f (#) |.g.|) . x
by FUNCT_1:47;
(f (#) |.g.|) . x = (f . x) * (|.g.| . x)
by A29, A7, A82, MESFUNC1:def 5;
then A84:
(f (#) |.g.|) . x = (f . x) * |.(g . x).|
by A16, A29, A7, A82, MESFUNC1:def 10;
(l0 (#) |.g.|) . x = l0 * (|.g.| . x)
by A29, A7, A81, A82, MESFUNC1:def 6;
then
(l0 (#) |.g.|) . x = l0 * |.(g . x).|
by A16, A29, A7, A82, MESFUNC1:def 10;
then
(f (#) |.g.|) . x <= (l0 (#) |.g.|) . x
by A29, A7, A33, A82, A84;
hence
((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x
by A29, A7, A42, A82, A83, FUNCT_1:47;
verum
end;
then A85:
((l0 (#) |.g.|) | E) - ((f (#) |.g.|) | E) is nonnegative
by Th1;
Integral (M,((k0 (#) |.g.|) | E)) = Integral (M,(k0 (#) (|.g.| | E)))
by Th2;
then A86:
Integral (M,((k0 (#) |.g.|) | E)) = k0 * (Integral (M,(|.g.| | E)))
by A27, MESFUNC5:110;
l0 (#) |.g.| is_integrable_on M
by A26, MESFUNC5:110;
then
(l0 (#) |.g.|) | E is_integrable_on M
by MESFUNC5:97;
then consider V2 being Element of S such that
A87:
V2 = (dom ((l0 (#) |.g.|) | E)) /\ (dom ((f (#) |.g.|) | E))
and
A88:
Integral (M,(((f (#) |.g.|) | E) | V2)) <= Integral (M,(((l0 (#) |.g.|) | E) | V2))
by A76, A85, Th3;
A89:
((f (#) |.g.|) | E) | V2 = (f (#) |.g.|) | E
by A29, A7, A42, A87, RELAT_1:68;
A90:
((l0 (#) |.g.|) | E) | V2 = (l0 (#) |.g.|) | E
by A29, A7, A42, A87, RELAT_1:68;
A91:
Integral (M,((f (#) |.g.|) | E)) < +infty
by A76, MESFUNC5:96;
A92:
((k0 (#) |.g.|) | E) | V1 = (k0 (#) |.g.|) | E
by A29, A7, A31, A78, RELAT_1:68;
ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) )
proof
per cases
( Integral (M,(|.g.| | E)) <> 0. or Integral (M,(|.g.| | E)) = 0. )
;
suppose A93:
Integral (
M,
(|.g.| | E))
<> 0.
;
ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) )reconsider c3 =
Integral (
M,
((f (#) |.g.|) | E)) as
Element of
REAL by A77, A91, XXREAL_0:14;
set c2 =
(Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E)));
A94:
Integral (
M,
(|.g.| | E))
< +infty
by A27, MESFUNC5:96;
A95:
-infty < Integral (
M,
(|.g.| | E))
by A27, MESFUNC5:96;
then reconsider c1 =
Integral (
M,
(|.g.| | E)) as
Element of
REAL by A94, XXREAL_0:14;
(Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) = c3 / c1
;
then reconsider c =
(Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E))) as
Element of
REAL by XREAL_0:def 1;
A96:
c3 * (c1 / c1) = (Integral (M,((f (#) |.g.|) | E))) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))))
by EXTREAL1:1;
(Integral (M,(|.g.| | E))) * ((Integral (M,((f (#) |.g.|) | E))) / (Integral (M,(|.g.| | E)))) = c1 * (c3 / c1)
by EXTREAL1:1;
then A97:
c * (Integral (M,(|.g.| | E))) = Integral (
M,
((f (#) |.g.|) | E))
by A93, A96, XXREAL_3:88;
A98:
Integral (
M,
(|.g.| | E))
> 0.
by A21, A22, A23, A93, MESFUNC2:27, MESFUNC5:92;
(sup F) * (Integral (M,(|.g.| | E))) = l0 * c1
by EXTREAL1:1;
then A99:
((sup F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (l0 * c1) / c1
;
(l0 * c1) / c1 = l0 * (c1 / c1)
;
then A100:
((sup F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))))
by A99, EXTREAL1:1;
(inf F) * (Integral (M,(|.g.| | E))) = k0 * c1
by EXTREAL1:1;
then A101:
((inf F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (k0 * c1) / c1
;
(k0 * c1) / c1 = k0 * (c1 / c1)
;
then A102:
((inf F) * (Integral (M,(|.g.| | E)))) / (Integral (M,(|.g.| | E))) = (inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E))))
by A101, EXTREAL1:1;
(sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = (sup F) * 1.
by A93, A95, A94, XXREAL_3:78;
then
(sup F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = sup F
by XXREAL_3:81;
then A103:
c <= sup F
by A51, A88, A89, A90, A98, A100, XXREAL_3:79;
(inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = (inf F) * 1.
by A93, A95, A94, XXREAL_3:78;
then
(inf F) * ((Integral (M,(|.g.| | E))) / (Integral (M,(|.g.| | E)))) = inf F
by XXREAL_3:81;
then
c >= inf F
by A86, A79, A92, A80, A98, A102, XXREAL_3:79;
hence
ex
c being
Element of
REAL st
(
c >= inf F &
c <= sup F &
Integral (
M,
((f (#) |.g.|) | E))
= c * (Integral (M,(|.g.| | E))) )
by A103, A97;
verum end; suppose A104:
Integral (
M,
(|.g.| | E))
= 0.
;
ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) )then
0. <= Integral (
M,
((f (#) |.g.|) | E))
by A29, A7, A31, A86, A78, A79, A80, RELAT_1:68;
then A105:
Integral (
M,
((f (#) |.g.|) | E))
= 0.
by A29, A7, A42, A51, A87, A88, A89, A104, RELAT_1:68;
consider y being
object such that A106:
y in F
by XBOOLE_0:def 1;
reconsider y =
y as
Element of
ExtREAL by A106;
A107:
y <= sup F
by A106, XXREAL_2:4;
inf F <= y
by A106, XXREAL_2:3;
then A108:
k0 <= sup F
by A107, XXREAL_0:2;
k0 * (Integral (M,(|.g.| | E))) = 0.
by A104;
hence
ex
c being
Element of
REAL st
(
c >= inf F &
c <= sup F &
Integral (
M,
((f (#) |.g.|) | E))
= c * (Integral (M,(|.g.| | E))) )
by A108, A105;
verum end; end;
end;
hence
( (f (#) g) | E is_integrable_on M & ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral (M,((f (#) |.g.|) | E)) = c * (Integral (M,(|.g.| | E))) ) )
by A44, A64, A74, A53, A66, MESFUNC5:102; verum