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 A1: ( (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 ) ; :: 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)) ) )
then consider E1 being Element of S such that
A2: ( E1 = dom g & g is_measurable_on E1 ) by MESFUNC5:def 17;
A3: ( E1 = dom |.g.| & |.g.| is_measurable_on E1 ) by A2, MESFUNC1:def 10, MESFUNC2:29;
then A4: ( g is_measurable_on E & |.g.| is_measurable_on E ) by A1, A2, MESFUNC1:34, XBOOLE_1:17;
A5: ( rng f is bounded_below & rng f is bounded_above ) by A1, XXREAL_2:def 11;
A6: f is real-valued by A1, Th16;
A7: rng f is Subset of REAL by A1, Th16, MESFUNC2:35;
then ( not +infty in rng f & not -infty in rng f ) ;
then ( rng f <> {+infty } & rng f <> {-infty } ) by TARSKI:def 1;
then reconsider k0 = inf F, l0 = sup F as Real by A1, A5, XXREAL_2:57, XXREAL_2:58;
( |.(inf F).| = abs k0 & |.(sup F).| = abs l0 ) by EXTREAL2:49;
then reconsider k1 = |.(inf F).|, l1 = |.(sup F).| as Real ;
A8: dom |.g.| = dom g by MESFUNC1:def 10;
A9: ( E c= dom f & E c= dom g ) by A1, XBOOLE_1:17;
then A10: E c= dom |.g.| by MESFUNC1:def 10;
A11: dom (f (#) g) = E by A1, MESFUNC1:def 5;
then A12: dom ((f (#) g) | E) = E by RELAT_1:91;
then A13: dom |.((f (#) g) | E).| = E by MESFUNC1:def 10;
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 A14: dom (((k1 + l1) (#) |.g.|) | E) = E by A10, RELAT_1:91;
A15: dom ((k1 + l1) (#) |.g.|) = dom |.g.| by MESFUNC1:def 6;
A16: dom (f (#) |.g.|) = (dom f) /\ (dom |.g.|) by MESFUNC1:def 5;
then A17: dom (f (#) |.g.|) = E by A1, MESFUNC1:def 10;
A18: dom ((f (#) |.g.|) | E) = (dom (f (#) |.g.|)) /\ E by RELAT_1:90;
A19: ( inf F is LowerBound of rng f & sup F is UpperBound of rng f ) by A1, XXREAL_2:def 3, XXREAL_2:def 4;
A20: for x being Element of X st x in E holds
|.(f . x).| <= |.(inf F).| + |.(sup F).|

proof

let x be Element of X; :: thesis: ( x in E implies |.(f . x).| <= |.(inf F).| + |.(sup F).| )
assume x in E ; :: thesis: |.(f . x).| <= |.(inf F).| + |.(sup F).|
then A21: f . x in rng f by A9, FUNCT_1:12;
then reconsider fx = f . x as Real by A7;
A22: ( k0 <= fx & fx <= l0 ) by A19, A21, XXREAL_2:def 1, XXREAL_2:def 2;
( l0 <= abs l0 & 0 <= abs k0 ) by COMPLEX1:132, COMPLEX1:162;
then ( l0 + (abs k0) <= (abs l0) + (abs k0) & l0 + 0 <= l0 + (abs k0) ) by XREAL_1:8;
then A23: l0 <= (abs l0) + (abs k0) by XXREAL_0:2;
0 <= abs l0 by COMPLEX1:132;
then A24: (- (abs k0)) - (abs l0) <= (- (abs k0)) - 0 by XREAL_1:12;
- (abs k0) <= k0 by COMPLEX1:162;
then (- (abs k0)) - (abs l0) <= k0 by A24, XXREAL_0:2;
then ( - ((abs k0) + (abs l0)) <= fx & fx <= (abs k0) + (abs l0) ) by A22, A23, XXREAL_0:2;
then A25: abs fx <= (abs k0) + (abs l0) by ABSVALUE:12;
( abs fx = |.(f . x).| & abs k0 = |.(inf F).| & abs l0 = |.(sup F).| ) by EXTREAL2:49;
hence |.(f . x).| <= |.(inf F).| + |.(sup F).| by A25, SUPINF_2:1; :: thesis: verum

end;

A26: |.g.| is_integrable_on M by A1, A2, MESFUNC5:106;
then A27: |.g.| | E is_integrable_on M by MESFUNC5:103;
(k1 + l1) (#) |.g.| is_integrable_on M by A26, MESFUNC5:116;
then A28: ((k1 + l1) (#) |.g.|) | E is_integrable_on M by MESFUNC5:103;
A29: f (#) g is_measurable_on E by A1, A4, A6, Th15;
(dom (f (#) g)) /\ E = E by A11;
then A30: (f (#) g) | E is_measurable_on E by A29, MESFUNC5:48;
A31: 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 A32: x in dom ((f (#) g) | E) ; :: thesis: |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x
then A33: ((f (#) g) | E) . x = (f (#) g) . x by FUNCT_1:70;
( dom (f | E) = E & dom (g | E) = E ) by A1, RELAT_1:91, XBOOLE_1:17;
then A34: ( (f | E) . x = f . x & (g | E) . x = g . x ) by A12, A32, FUNCT_1:70;
0 <= |.((g | E) . x).| by EXTREAL2:51;
then A35: |.((f | E) . x).| * |.((g | E) . x).| <= (|.(inf F).| + |.(sup F).|) * |.((g | E) . x).| by A12, A20, A32, A34, XXREAL_3:82;
A36: (((k1 + l1) (#) |.g.|) | E) . x = ((k1 + l1) (#) |.g.|) . x by A12, A14, A32, FUNCT_1:70;
|.((f (#) g) . x).| = |.((f . x) * (g . x)).| by A11, A12, A32, MESFUNC1:def 5;
then A37: |.(((f (#) g) | E) . x).| = |.((f | E) . x).| * |.((g | E) . x).| by A33, A34, EXTREAL2:56;
((k1 + l1) (#) |.g.|) . x = (R_EAL (k1 + l1)) * (|.g.| . x) by A10, A12, A15, A32, MESFUNC1:def 6;
then (((k1 + l1) (#) |.g.|) | E) . x = (R_EAL (k1 + l1)) * |.((g | E) . x).| by A10, A12, A32, A34, A36, MESFUNC1:def 10;
hence |.(((f (#) g) | E) . x).| <= (((k1 + l1) (#) |.g.|) | E) . x by A35, A37, SUPINF_2:1; :: thesis: verum

end;

then (f (#) g) | E is_integrable_on M by A12, A14, A28, A30, MESFUNC5:108;
then A38: |.((f (#) g) | E).| is_integrable_on M by A12, A30, MESFUNC5:106;
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 A39: 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 A1, A8, A39, MESFUNC2:def 1; :: thesis: verum

end;

then A40: |.g.| is real-valued by MESFUNC2:def 1;
(dom f) /\ (dom |.g.|) = E by A1, MESFUNC1:def 10;
then A41: f (#) |.g.| is_measurable_on E by A1, A4, A6, A40, Th15;
(dom (f (#) |.g.|)) /\ E = E by A17;
then A42: (f (#) |.g.|) | E is_measurable_on E by A41, MESFUNC5:48;
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 A43: x in dom ((f (#) |.g.|) | E) ; :: thesis: |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x
then |.((f (#) |.g.|) . x).| = |.((f . x) * (|.g.| . x)).| by A17, A18, MESFUNC1:def 5
.= |.((f . x) * |.(g . x).|).| by A1, A8, A9, A16, A18, A43, MESFUNC1:def 10
.= |.(f . x).| * |.|.(g . x).|.| by EXTREAL2:56
.= |.(f . x).| * |.(g . x).| by EXTREAL2:70 ;
then A44: |.((f (#) |.g.|) . x).| = |.((f . x) * (g . x)).| by EXTREAL2:56;
dom |.(f (#) g).| = E by A11, MESFUNC1:def 10;
then A45: |.(f (#) g).| . x = |.((f (#) g) . x).| by A17, A18, A43, MESFUNC1:def 10;
A46: ((f (#) |.g.|) | E) . x = (f (#) |.g.|) . x by A43, FUNCT_1:70;
|.(((f (#) g) | E) . x).| = |.((f (#) g) . x).| by A12, A17, A18, A43, FUNCT_1:70;
then |.((f (#) g) | E).| . x = |.(f (#) g).| . x by A13, A17, A18, A43, A45, MESFUNC1:def 10;
hence |.(((f (#) |.g.|) | E) . x).| <= |.((f (#) g) | E).| . x by A11, A17, A18, A43, A44, A45, A46, MESFUNC1:def 5; :: thesis: verum

end;

then A47: (f (#) |.g.|) | E is_integrable_on M by A13, A17, A18, A38, A42, MESFUNC5:108;
A48: 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).| ) )
assume x in E ; :: thesis: ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| )
then f . x in rng f by A9, FUNCT_1:12;
then A49: ( inf F <= f . x & f . x <= sup F ) by A19, XXREAL_2:def 1, XXREAL_2:def 2;
0 <= |.(g . x).| by EXTREAL2:51;
hence ( (inf F) * |.(g . x).| <= (f . x) * |.(g . x).| & (f . x) * |.(g . x).| <= (sup F) * |.(g . x).| ) by A49, XXREAL_3:82; :: thesis: verum

end;

A50: ( dom (k0 (#) |.g.|) = dom |.g.| & dom (l0 (#) |.g.|) = dom |.g.| ) by MESFUNC1:def 6;
then A51: ( dom ((k0 (#) |.g.|) | E) = E & dom ((l0 (#) |.g.|) | E) = E ) by A10, RELAT_1:91;
A52: dom (f (#) |.g.|) c= dom (l0 (#) |.g.|) by A16, A50, XBOOLE_1:17;
( Integral M,((k0 (#) |.g.|) | E) = Integral M,(k0 (#) (|.g.| | E)) & Integral M,((l0 (#) |.g.|) | E) = Integral M,(l0 (#) (|.g.| | E)) ) by Th2;
then A53: ( Integral M,((k0 (#) |.g.|) | E) = (R_EAL k0) * (Integral M,(|.g.| | E)) & Integral M,((l0 (#) |.g.|) | E) = (R_EAL l0) * (Integral M,(|.g.| | E)) ) by A27, MESFUNC5:116;
k0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:116;
then A54: (k0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:103;
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 A55: x in dom ((k0 (#) |.g.|) | E) ; :: thesis: ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x
then ( (k0 (#) |.g.|) . x = (R_EAL k0) * (|.g.| . x) & (f (#) |.g.|) . x = (f . x) * (|.g.| . x) ) by A10, A17, A50, A51, MESFUNC1:def 5, MESFUNC1:def 6;
then ( (k0 (#) |.g.|) . x = (R_EAL k0) * |.(g . x).| & (f (#) |.g.|) . x = (f . x) * |.(g . x).| ) by A10, A51, A55, MESFUNC1:def 10;
then A56: (k0 (#) |.g.|) . x <= (f (#) |.g.|) . x by A48, A51, A55;
((k0 (#) |.g.|) | E) . x = (k0 (#) |.g.|) . x by A55, FUNCT_1:70;
hence ((k0 (#) |.g.|) | E) . x <= ((f (#) |.g.|) | E) . x by A17, A18, A51, A55, A56, FUNCT_1:70; :: thesis: verum

end;

then ((f (#) |.g.|) | E) - ((k0 (#) |.g.|) | E) is nonnegative by Th1;
then consider V1 being Element of S such that
A57: ( V1 = (dom ((k0 (#) |.g.|) | E)) /\ (dom ((f (#) |.g.|) | E)) & Integral M,(((k0 (#) |.g.|) | E) | V1) <= Integral M,(((f (#) |.g.|) | E) | V1) ) by A47, A54, Th3;
A58: ( ((k0 (#) |.g.|) | E) | V1 = (k0 (#) |.g.|) | E & ((f (#) |.g.|) | E) | V1 = (f (#) |.g.|) | E ) by A17, A18, A51, A57, RELAT_1:97;
l0 (#) |.g.| is_integrable_on M by A26, MESFUNC5:116;
then A59: (l0 (#) |.g.|) | E is_integrable_on M by MESFUNC5:103;
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 A60: x in dom ((f (#) |.g.|) | E) ; :: thesis: ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x
then ( (f (#) |.g.|) . x = (f . x) * (|.g.| . x) & (l0 (#) |.g.|) . x = (R_EAL l0) * (|.g.| . x) ) by A17, A18, A52, MESFUNC1:def 5, MESFUNC1:def 6;
then ( (f (#) |.g.|) . x = (f . x) * |.(g . x).| & (l0 (#) |.g.|) . x = (R_EAL l0) * |.(g . x).| ) by A10, A17, A18, A60, MESFUNC1:def 10;
then A61: (f (#) |.g.|) . x <= (l0 (#) |.g.|) . x by A17, A18, A48, A60;
((f (#) |.g.|) | E) . x = (f (#) |.g.|) . x by A60, FUNCT_1:70;
hence ((f (#) |.g.|) | E) . x <= ((l0 (#) |.g.|) | E) . x by A17, A18, A51, A60, A61, FUNCT_1:70; :: thesis: verum

end;

then ((l0 (#) |.g.|) | E) - ((f (#) |.g.|) | E) is nonnegative by Th1;
then consider V2 being Element of S such that
A62: ( V2 = (dom ((l0 (#) |.g.|) | E)) /\ (dom ((f (#) |.g.|) | E)) & Integral M,(((f (#) |.g.|) | E) | V2) <= Integral M,(((l0 (#) |.g.|) | E) | V2) ) by A47, A59, Th3;
A63: ( ((f (#) |.g.|) | E) | V2 = (f (#) |.g.|) | E & ((l0 (#) |.g.|) | E) | V2 = (l0 (#) |.g.|) | E ) by A17, A18, A51, A62, RELAT_1:97;
A64: ( -infty < Integral M,((f (#) |.g.|) | E) & Integral M,((f (#) |.g.|) | E) < +infty ) by A47, MESFUNC5:102;
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 A65: 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 A66: Integral M,(|.g.| | E) > 0. by A3, MESFUNC5:98;
A67: ( -infty < Integral M,(|.g.| | E) & Integral M,(|.g.| | E) < +infty ) by A27, MESFUNC5:102;
then reconsider c1 = Integral M,(|.g.| | E) as Real by XXREAL_0:14;
A68: (Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E)) = c1 / c1 by EXTREAL1:32;
( (inf F) * (Integral M,(|.g.| | E)) = k0 * c1 & (sup F) * (Integral M,(|.g.| | E)) = l0 * c1 ) by EXTREAL1:13;
then A69: ( ((inf F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (k0 * c1) / c1 & ((sup F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (l0 * c1) / c1 ) by EXTREAL1:32;
( (k0 * c1) / c1 = k0 * (c1 / c1) & (l0 * c1) / c1 = l0 * (c1 / c1) ) ;
then A70: ( ((inf F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (inf F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) & ((sup F) * (Integral M,(|.g.| | E))) / (Integral M,(|.g.| | E)) = (sup F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) ) by A68, A69, EXTREAL1:13;
( (inf F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = (inf F) * 1. & (sup F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = (sup F) * 1. ) by A65, A67, XXREAL_3:89;
then A71: ( (inf F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = inf F & (sup F) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) = sup F ) by XXREAL_3:92;
set c2 = (Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E));
reconsider c3 = Integral M,((f (#) |.g.|) | E) as Real by A64, 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 ;
A72: ( c >= inf F & c <= sup F ) by A53, A57, A58, A62, A63, A66, A70, A71, XXREAL_3:90;
( (Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E)) = c3 / c1 & (Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E)) = c1 / c1 ) by EXTREAL1:32;
then ( (Integral M,(|.g.| | E)) * ((Integral M,((f (#) |.g.|) | E)) / (Integral M,(|.g.| | E))) = c1 * (c3 / c1) & c3 * (c1 / c1) = (Integral M,((f (#) |.g.|) | E)) * ((Integral M,(|.g.| | E)) / (Integral M,(|.g.| | E))) ) by EXTREAL1:13;
then (R_EAL c) * (Integral M,(|.g.| | E)) = Integral M,((f (#) |.g.|) | E) by A65, A67, XXREAL_3:99;
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 A72; :: thesis: verum

end;

suppose A73: 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)) )

consider y being set such that
A74: y in F by XBOOLE_0:def 1;
reconsider y = y as Element of ExtREAL by A74;
( inf F <= y & y <= sup F ) by A74, XXREAL_2:3, XXREAL_2:4;
then A75: ( inf F <= k0 & k0 <= sup F ) by XXREAL_0:2;
0. <= Integral M,((f (#) |.g.|) | E) by A53, A57, A58, A73;
then A76: Integral M,((f (#) |.g.|) | E) = 0. by A53, A62, A63, A73;
(R_EAL k0) * (Integral M,(|.g.| | E)) = 0. by A73;
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 A75, A76; :: 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 A12, A14, A28, A30, A31, MESFUNC5:108; :: thesis: verum