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 real-valued & f is_measurable_on E & rng f is 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) = (R_EAL 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 real-valued & f is_measurable_on E & rng f is 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) = (R_EAL 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 real-valued & f is_measurable_on E & rng f is 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) = (R_EAL 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 real-valued & f is_measurable_on E & rng f is 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) = (R_EAL 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 real-valued & f is_measurable_on E & rng f is 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) = (R_EAL c) * (Integral M,(|.g.| | E)) ) )
let F be non empty Subset of ExtREAL ; :: thesis: ( (dom f) /\ (dom g) = E & rng f = F & g is real-valued & f is_measurable_on E & rng f is 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) = (R_EAL c) * (Integral M,(|.g.| | E)) ) ) )
assume that
A1: (dom f) /\ (dom g) = E and
A2: rng f = F and
A3: g is real-valued and
A4: f is_measurable_on E and
A5: rng f is 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) = (R_EAL c) * (Integral M,(|.g.| | E)) ) )
A7: dom ((f (#) |.g.|) | E) = (dom (f (#) |.g.|)) /\ E by RELAT_1:90;
A8: rng f is Subset of REAL by A5, Th16, MESFUNC2:35;
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 Real by A2, A10, A9, A11, XXREAL_2:57, XXREAL_2:58;
A12: |.(sup F).| = abs l0 by EXTREAL2:49;
|.(inf F).| = abs k0 by EXTREAL2:49;
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).| by EXTREAL2:70;
hence |.(|.g.| . x).| < +infty by A3, A17, A18, MESFUNC2:def 1; :: thesis: verum

end;

then A19: |.g.| is real-valued by MESFUNC2:def 1;
A20: f is real-valued by A5, Th16;
consider E1 being Element of S such that
A21: E1 = dom g and
A22: g is_measurable_on E1 by A6, MESFUNC5:def 17;
A23: E1 = dom |.g.| by A21, MESFUNC1:def 10;
|.g.| is_measurable_on E1 by A21, A22, MESFUNC2:29;
then A24: |.g.| is_measurable_on E by A1, A21, MESFUNC1:34, XBOOLE_1:17;
(dom f) /\ (dom |.g.|) = E by A1, MESFUNC1:def 10;
then A25: f (#) |.g.| is_measurable_on E by A4, A24, A20, A19, Th15;
A26: |.g.| is_integrable_on M by A6, A21, A22, MESFUNC5:106;
then A27: |.g.| | E is_integrable_on M by MESFUNC5:103;
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:91;
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 EXTREAL2:51;
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:12, XXREAL_2:def 1;
inf F <= f . x by A13, A32, A35, FUNCT_1:12, 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:82; :: 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:70;
(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 = (R_EAL k0) * (|.g.| . x) by A16, A30, A31, A37, MESFUNC1:def 6;
then (k0 (#) |.g.|) . x = (R_EAL 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:70; :: 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:91;
A43: dom (f (#) g) = E by A1, MESFUNC1:def 5;
then A44: dom ((f (#) g) | E) = E by RELAT_1:91;
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:70;
|.((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 EXTREAL2:56
.= |.(f . x).| * |.(g . x).| by EXTREAL2:70 ;
then A49: |.((f (#) |.g.|) . x).| = |.((f . x) * (g . x)).| by EXTREAL2:56;
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:70;
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) = (R_EAL l0) * (Integral M,(|.g.| | E)) by A27, MESFUNC5:116;
A52: (dom (f (#) g)) /\ E = E by A43;
g is_measurable_on E by A1, A21, A22, MESFUNC1:34, XBOOLE_1:17;
then f (#) g is_measurable_on E by A1, A3, A4, A20, Th15;
then A53: (f (#) g) | E is_measurable_on E by A52, MESFUNC5:48;
A54: for x being Element of X st x in E holds
|.(f . x).| <= |.(inf F).| + |.(sup F).|

proof

0 <= abs k0 by COMPLEX1:132;
then A55: l0 + 0 <= l0 + (abs k0) by XREAL_1:8;
l0 <= abs l0 by COMPLEX1:162;
then l0 + (abs k0) <= (abs l0) + (abs k0) by XREAL_1:8;
then A56: l0 <= (abs l0) + (abs k0) by A55, XXREAL_0:2;
0 <= abs l0 by COMPLEX1:132;
then A57: (- (abs k0)) - (abs l0) <= (- (abs k0)) - 0 by XREAL_1:12;
- (abs k0) <= k0 by COMPLEX1:162;
then A58: (- (abs k0)) - (abs 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: abs k0 = |.(inf F).| by EXTREAL2:49;
assume A60: x in E ; :: thesis: |.(f . x).| <= |.(inf F).| + |.(sup F).|
then f . x in rng f by A13, FUNCT_1:12;
then reconsider fx = f . x as Real by A8;
A61: abs l0 = |.(sup F).| by EXTREAL2:49;
fx <= l0 by A13, A14, A60, FUNCT_1:12, XXREAL_2:def 1;
then A62: fx <= (abs k0) + (abs l0) by A56, XXREAL_0:2;
k0 <= fx by A13, A32, A60, FUNCT_1:12, XXREAL_2:def 2;
then - ((abs k0) + (abs l0)) <= fx by A58, XXREAL_0:2;
then A63: abs fx <= (abs k0) + (abs l0) by A62, ABSVALUE:12;
abs fx = |.(f . x).| by EXTREAL2:49;
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:91;
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:70;
dom (f | E) = E by A1, RELAT_1:91, XBOOLE_1:17;
then A69: (f | E) . x = f . x by A44, A67, FUNCT_1:70;
dom (g | E) = E by A1, RELAT_1:91, XBOOLE_1:17;
then A70: (g | E) . x = g . x by A44, A67, FUNCT_1:70;
0 <= |.((g | E) . x).| by EXTREAL2:51;
then A71: |.((f | E) . x).| * |.((g | E) . x).| <= (|.(inf F).| + |.(sup F).|) * |.((g | E) . x).| by A44, A54, A67, A69, XXREAL_3:82;
A72: (((k1 + l1) (#) |.g.|) | E) . x = ((k1 + l1) (#) |.g.|) . x by A44, A64, A67, FUNCT_1:70;
|.((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, EXTREAL2:56;
((k1 + l1) (#) |.g.|) . x = (R_EAL (k1 + l1)) * (|.g.| . x) by A16, A44, A65, A67, MESFUNC1:def 6;
then (((k1 + l1) (#) |.g.|) | E) . x = (R_EAL (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:116;
then A74: ((k1 + l1) (#) |.g.|) | E is_integrable_on M by MESFUNC5:103;
then (f (#) g) | E is_integrable_on M by A44, A64, A53, A66, MESFUNC5:108;
then A75: |.((f (#) g) | E).| is_integrable_on M by A44, A53, MESFUNC5:106;
(dom (f (#) |.g.|)) /\ E = E by A29;
then (f (#) |.g.|) | E is_measurable_on E by A25, MESFUNC5:48;
then A76: (f (#) |.g.|) | E is_integrable_on M by A45, A29, A7, A75, A46, MESFUNC5:108;
then A77: -infty < Integral M,((f (#) |.g.|) | E) by MESFUNC5:102;
k0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:116;
then (k0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:103;
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:97;
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:70;
(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 = (R_EAL l0) * (|.g.| . x) by A29, A7, A81, A82, MESFUNC1:def 6;
then (l0 (#) |.g.|) . x = (R_EAL 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:70; :: 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) = (R_EAL k0) * (Integral M,(|.g.| | E)) by A27, MESFUNC5:116;
l0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:116;
then (l0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:103;
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:97;
A90: ((l0 (#) |.g.|) | E) | V2 = (l0 (#) |.g.|) | E by A29, A7, A42, A87, RELAT_1:97;
A91: Integral M,((f (#) |.g.|) | E) < +infty by A76, MESFUNC5:102;
A92: ((k0 (#) |.g.|) | E) | V1 = (k0 (#) |.g.|) | E by A29, A7, A31, A78, RELAT_1:97;
ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral M,((f (#) |.g.|) | E) = (R_EAL 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) = (R_EAL c) * (Integral M,(|.g.| | E)) )

reconsider c3 = Integral M,((f (#) |.g.|) | E) as 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:102;
A95: -infty < Integral M,(|.g.| | E) by A27, MESFUNC5:102;
then reconsider c1 = Integral M,(|.g.| | E) as Real by A94, XXREAL_0:14;
(Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E)) = c3 / c1 by EXTREAL1:32;
then reconsider c = (Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E)) as Element of REAL ;
A96: (Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E)) = c1 / c1 by EXTREAL1:32;
(Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E)) = c1 / c1 by EXTREAL1:32;
then A97: c3 * (c1 / c1) = (Integral M,((f (#) |.g.|) | E)) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) by EXTREAL1:13;
(Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E)) = c3 / c1 by EXTREAL1:32;
then (Integral M,(|.g.| | E)) * ((Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E))) = c1 * (c3 / c1) by EXTREAL1:13;
then A98: (R_EAL c) * (Integral M,(|.g.| | E)) = Integral M,((f (#) |.g.|) | E) by A93, A97, XXREAL_3:99;
A99: Integral M,(|.g.| | E) > 0. by A21, A22, A23, A93, MESFUNC2:29, MESFUNC5:98;
(sup F) * (Integral M,(|.g.| | E)) = l0 * c1 by EXTREAL1:13;
then A100: ((sup F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (l0 * c1) / c1 by EXTREAL1:32;
(l0 * c1) / c1 = l0 * (c1 / c1) ;
then A101: ((sup F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (sup F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) by A96, A100, EXTREAL1:13;
(inf F) * (Integral M,(|.g.| | E)) = k0 * c1 by EXTREAL1:13;
then A102: ((inf F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (k0 * c1) / c1 by EXTREAL1:32;
(k0 * c1) / c1 = k0 * (c1 / c1) ;
then A103: ((inf F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (inf F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) by A96, A102, EXTREAL1:13;
(sup F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = (sup F) * 1. by A93, A95, A94, XXREAL_3:89;
then (sup F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = sup F by XXREAL_3:92;
then A104: c <= sup F by A51, A88, A89, A90, A99, A101, XXREAL_3:90;
(inf F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = (inf F) * 1. by A93, A95, A94, XXREAL_3:89;
then (inf F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = inf F by XXREAL_3:92;
then c >= inf F by A86, A79, A92, A80, A99, A103, XXREAL_3:90;
hence ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral M,((f (#) |.g.|) | E) = (R_EAL c) * (Integral M,(|.g.| | E)) ) by A104, A98; :: thesis: verum

end;

suppose A105: Integral M,(|.g.| | E) = 0. ; :: thesis: ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral M,((f (#) |.g.|) | E) = (R_EAL c) * (Integral M,(|.g.| | E)) )

then 0. <= Integral M,((f (#) |.g.|) | E) by A29, A7, A31, A86, A78, A79, A80, RELAT_1:97;
then A106: Integral M,((f (#) |.g.|) | E) = 0. by A29, A7, A42, A51, A87, A88, A89, A105, RELAT_1:97;
consider y being set such that
A107: y in F by XBOOLE_0:def 1;
reconsider y = y as Element of ExtREAL by A107;
A108: y <= sup F by A107, XXREAL_2:4;
inf F <= y by A107, XXREAL_2:3;
then A109: k0 <= sup F by A108, XXREAL_0:2;
(R_EAL k0) * (Integral M,(|.g.| | E)) = 0. by A105;
hence ex c being Element of REAL st
( c >= inf F & c <= sup F & Integral M,((f (#) |.g.|) | E) = (R_EAL c) * (Integral M,(|.g.| | E)) ) by A109, A106; :: 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) = (R_EAL c) * (Integral M,(|.g.| | E)) ) ) by A44, A64, A74, A53, A66, MESFUNC5:108; :: thesis: verum