let X be non empty set ; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: 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; :: thesis: ( (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 ; :: thesis: ( (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
proof
let x be Element of X; :: thesis: ( x in dom |.g.| implies |.(|.g.| . x).| < +infty )
assume A18: x in dom |.g.| ; :: thesis: |.(|.g.| . x).| < +infty
then |.(|.g.| . x).| = |.|.(g . x).|.| by MESFUNC1:def 10;
then |.(|.g.| . x).| = |.(g . x).| ;
hence |.(|.g.| . x).| < +infty by A3, A17, A18, MESFUNC2:def 1; :: thesis: verum
end;
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).| )
proof
let x be Element of X; :: thesis: ( x in E implies ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) )
A34: 0 <= |.(g . x).| by EXTREAL1:14;
assume A35: x in E ; :: thesis: ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| )
then A36: f . x <= sup F by A13, A14, FUNCT_1:3, XXREAL_2:def 1;
inf F <= f . x by A13, A32, A35, FUNCT_1:3, XXREAL_2:def 2;
hence ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) by A36, A34, XXREAL_3:71; :: thesis: verum
end;
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; :: thesis: ( x in dom ((k0 (#) |.g.|) | E) implies ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x )
assume A37: x in dom ((k0 (#) |.g.|) | E) ; :: thesis: ((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; :: thesis: 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; :: thesis: ( x in dom ((f (#) |.g.|) | E) implies |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x )
assume A47: x in dom ((f (#) |.g.|) | E) ; :: thesis: |.(((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; :: thesis: 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; :: thesis: ( x in E implies |.(f . x).| <= |.(inf F).| + |.(sup F).| )
A59: |.k0.| = |.(inf F).| by EXTREAL1:12;
assume A60: x in E ; :: thesis: |.(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; :: thesis: 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; :: thesis: ( x in dom ((f (#) g) | E) implies |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x )
assume A67: x in dom ((f (#) g) | E) ; :: thesis: |.(((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; :: thesis: 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; :: thesis: ( x in dom ((f (#) |.g.|) | E) implies ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x )
assume A82: x in dom ((f (#) |.g.|) | E) ; :: thesis: ((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; :: thesis: 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. ; :: thesis: 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; :: thesis: verum
end;
suppose A104: Integral (M,(|.g.| | E)) = 0. ; :: thesis: 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; :: thesis: 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; :: thesis: verum