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,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,n holds
ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,n holds
ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,n holds
ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let f, g be PartFunc of X,REAL ; :: thesis: for m, n being positive Real st (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,n holds
ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
let m, n be positive Real; :: thesis: ( (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,n implies ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) )
assume A1: ( (1 / m) + (1 / n) = 1 & f in Lp_Functions M,m & g in Lp_Functions M,n ) ; :: thesis: ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )
then A2: ( m > 1 & n > 1 ) by Lm300;
consider f1 being PartFunc of X,REAL such that
A4: ( f = f1 & ex NDf being Element of S st
( M . (NDf ` ) = 0 & dom f1 = NDf & f1 is_measurable_on NDf & (abs f1) to_power m is_integrable_on M ) ) by A1;
consider EDf being Element of S such that
A5: ( M . (EDf ` ) = 0 & dom f1 = EDf & f1 is_measurable_on EDf ) by A4;
consider g1 being PartFunc of X,REAL such that
A6: ( g = g1 & ex NDg being Element of S st
( M . (NDg ` ) = 0 & dom g1 = NDg & g1 is_measurable_on NDg & (abs g1) to_power n is_integrable_on M ) ) by A1;
consider EDg being Element of S such that
A7: ( M . (EDg ` ) = 0 & dom g1 = EDg & g1 is_measurable_on EDg ) by A6;
set u = (abs f1) to_power m;
set v = (abs g1) to_power n;
A8: ( 0 <= Integral M,((abs f1) to_power m) & 0 <= Integral M,((abs g1) to_power n) ) by A4, A6, A1, Lm15;
reconsider s1 = Integral M,((abs f1) to_power m), s2 = Integral M,((abs g1) to_power n) as Real by A4, A6, A1, Lm15;
A9: ( dom f1 = dom (abs f1) & dom g1 = dom (abs g1) ) by VALUED_1:def 11;
reconsider Nf = EDf ` , Ng = EDg ` as Element of S by MEASURE1:66;
set t1 = s1 to_power (1 / m);
set t2 = s2 to_power (1 / n);
set E = EDf /\ EDg;
A11: (EDf /\ EDg) ` = (EDf ` ) \/ (EDg ` ) by XBOOLE_1:54;
( Nf is measure_zero of M & Ng is measure_zero of M ) by A5, A7, MEASURE1:def 13;
then A13: (EDf /\ EDg) ` is measure_zero of M by A11, MEASURE1:70;
A14: dom (f1 (#) g1) = EDf /\ EDg by A5, A7, VALUED_1:def 4;
( f1 is_measurable_on EDf /\ EDg & g1 is_measurable_on EDf /\ EDg ) by A5, A7, MESFUNC6:16, XBOOLE_1:17;
then A15: f1 (#) g1 is_measurable_on EDf /\ EDg by A5, A7, MESFUN7C:31;
A16: f1 (#) g1 in L1_Functions M by A1, A4, A6, Th001a;
then A17: ex fg1 being PartFunc of X,REAL st
( fg1 = f1 (#) g1 & ex ND being Element of S st
( M . ND = 0 & dom fg1 = ND ` & fg1 is_integrable_on M ) ) ;
then A18: ( Integral M,(abs (f1 (#) g1)) in REAL & abs (f1 (#) g1) is_integrable_on M ) by LPSPACE1:44;

per cases ( ( s1 = 0 & s2 >= 0 ) or ( s1 > 0 & s2 = 0 ) or ( s1 <> 0 & s2 <> 0 ) ) by A4, A6, A1, Lm15;

suppose A19: ( s1 = 0 & s2 >= 0 ) ; :: thesis: ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

f1 in Lp_Functions M,m by A4;
then f1 a.e.= X --> 0 ,M by A19, Lm261;
then consider Nf1 being Element of S such that
A20: ( M . Nf1 = 0 & f1 | (Nf1 ` ) = (X --> 0 ) | (Nf1 ` ) ) by LPSPACE1:def 10;
reconsider Z = ((EDf /\ EDg) \ Nf1) ` as Element of S by MEASURE1:66;
A21: ((EDf /\ EDg) \ Nf1) ` = ((EDf /\ EDg) ` ) \/ Nf1 by SUBSET_1:33;
Nf1 is measure_zero of M by A20, MEASURE1:def 13;
then Z is measure_zero of M by A13, A21, MEASURE1:70;
then A22: M . Z = 0 by MEASURE1:def 13;
dom (X --> 0 ) = X by FUNCOP_1:19;
then A23: dom ((X --> 0 ) | (Z ` )) = Z ` by RELAT_1:91;
A24: dom ((f1 (#) g1) | (Z ` )) = Z ` by A14, RELAT_1:91, XBOOLE_1:36;
for x being set st x in dom ((f1 (#) g1) | (Z ` )) holds
((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x

proof

let x be set ; :: thesis: ( x in dom ((f1 (#) g1) | (Z ` )) implies ((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x )
assume A25: x in dom ((f1 (#) g1) | (Z ` )) ; :: thesis: ((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x
then ( x in X & not x in Nf1 ) by A24, XBOOLE_0:def 5;
then x in Nf1 ` by XBOOLE_0:def 5;
then ( f1 . x = (f1 | (Nf1 ` )) . x & (X --> 0 ) . x = ((X --> 0 ) | (Nf1 ` )) . x ) by FUNCT_1:72;
then A26: f1 . x = 0 by A20, A25, FUNCOP_1:13;
A27: dom ((f1 (#) g1) | (Z ` )) c= dom (f1 (#) g1) by RELAT_1:89;
((f1 (#) g1) | (Z ` )) . x = (f1 (#) g1) . x by A25, FUNCT_1:70
.= (f1 . x) * (g1 . x) by A25, A27, VALUED_1:def 4
.= ((Z ` ) --> 0 ) . x by A25, A24, A26, FUNCOP_1:13
.= ((X /\ (Z ` )) --> 0 ) . x by XBOOLE_1:28 ;
hence ((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x by FUNCOP_1:18; :: thesis: verum

end;

then (f1 (#) g1) | (Z ` ) = (X --> 0 ) | (Z ` ) by A23, A24, FUNCT_1:def 17;
then A28: f1 (#) g1 a.e.= X --> 0 ,M by A22, LPSPACE1:def 10;
X --> 0 in L1_Functions M by LmDef1;
then Integral M,(abs (f1 (#) g1)) = Integral M,(abs (X --> 0 )) by A16, A28, LPSPACE1:45;
then A29: Integral M,(abs (f1 (#) g1)) = 0 by LPSPACE1:55;
(s1 to_power (1 / m)) * (s2 to_power (1 / n)) = 0 * (s2 to_power (1 / n)) by A19, POWER:def 2;
hence ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) by A4, A6, A29; :: thesis: verum

end;

suppose A30: ( s1 > 0 & s2 = 0 ) ; :: thesis: ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

g1 in Lp_Functions M,n by A6;
then g1 a.e.= X --> 0 ,M by A30, Lm261;
then consider Ng1 being Element of S such that
A31: ( M . Ng1 = 0 & g1 | (Ng1 ` ) = (X --> 0 ) | (Ng1 ` ) ) by LPSPACE1:def 10;
reconsider Z = ((EDf /\ EDg) \ Ng1) ` as Element of S by MEASURE1:66;
A32: ((EDf /\ EDg) \ Ng1) ` = ((EDf /\ EDg) ` ) \/ Ng1 by SUBSET_1:33;
Ng1 is measure_zero of M by A31, MEASURE1:def 13;
then Z is measure_zero of M by A13, A32, MEASURE1:70;
then A33: M . Z = 0 by MEASURE1:def 13;
dom (X --> 0 ) = X by FUNCOP_1:19;
then A34: dom ((X --> 0 ) | (Z ` )) = Z ` by RELAT_1:91;
A35: dom ((f1 (#) g1) | (Z ` )) = Z ` by A14, RELAT_1:91, XBOOLE_1:36;
for x being set st x in dom ((f1 (#) g1) | (Z ` )) holds
((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x

proof

let x be set ; :: thesis: ( x in dom ((f1 (#) g1) | (Z ` )) implies ((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x )
assume A36: x in dom ((f1 (#) g1) | (Z ` )) ; :: thesis: ((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x
then ( x in X & not x in Ng1 ) by A35, XBOOLE_0:def 5;
then x in Ng1 ` by XBOOLE_0:def 5;
then ( g1 . x = (g1 | (Ng1 ` )) . x & (X --> 0 ) . x = ((X --> 0 ) | (Ng1 ` )) . x ) by FUNCT_1:72;
then A37: g1 . x = 0 by A31, A36, FUNCOP_1:13;
A38: dom ((f1 (#) g1) | (Z ` )) c= dom (f1 (#) g1) by RELAT_1:89;
((f1 (#) g1) | (Z ` )) . x = (f1 (#) g1) . x by A36, FUNCT_1:70
.= (f1 . x) * (g1 . x) by A36, A38, VALUED_1:def 4
.= ((Z ` ) --> 0 ) . x by A36, A35, A37, FUNCOP_1:13
.= ((X /\ (Z ` )) --> 0 ) . x by XBOOLE_1:28 ;
hence ((f1 (#) g1) | (Z ` )) . x = ((X --> 0 ) | (Z ` )) . x by FUNCOP_1:18; :: thesis: verum

end;

then (f1 (#) g1) | (Z ` ) = (X --> 0 ) | (Z ` ) by A34, A35, FUNCT_1:def 17;
then A39: f1 (#) g1 a.e.= X --> 0 ,M by A33, LPSPACE1:def 10;
X --> 0 in L1_Functions M by LmDef1;
then Integral M,(abs (f1 (#) g1)) = Integral M,(abs (X --> 0 )) by A16, A39, LPSPACE1:45;
then A40: Integral M,(abs (f1 (#) g1)) = 0 by LPSPACE1:55;
(s1 to_power (1 / m)) * (s2 to_power (1 / n)) = (s1 to_power (1 / m)) * 0 by A30, POWER:def 2;
hence ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) by A4, A6, A40; :: thesis: verum

end;

suppose A41: ( s1 <> 0 & s2 <> 0 ) ; :: thesis: ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) )

then A42: ( s1 to_power (1 / m) > 0 & s2 to_power (1 / n) > 0 ) by A8, POWER:39;
then A43: abs (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) = 1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) by ABSVALUE:def 1;
set w = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1);
set F = (1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m);
set G = (1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n);
set z = ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n));
A44: ( dom ((1 / (s1 to_power (1 / m))) (#) (abs f1)) = dom (abs f1) & dom ((1 / (s2 to_power (1 / n))) (#) (abs g1)) = dom (abs g1) ) by VALUED_1:def 5;
( dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) = dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) & dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) = dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) ) by VALUED_1:def 5;
then A45: ( dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) = dom (abs f1) & dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) = dom (abs g1) ) by A44, MESFUN6C:def 6;
then A46: dom (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) = (dom (abs f1)) /\ (dom (abs g1)) by VALUED_1:def 1;
( ((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m = ((1 / (s1 to_power (1 / m))) to_power m) (#) ((abs f1) to_power m) & ((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n = ((1 / (s2 to_power (1 / n))) to_power n) (#) ((abs g1) to_power n) ) by A42, Lm001f;
then A47: ( ((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m is_integrable_on M & ((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n is_integrable_on M ) by A4, A6, MESFUNC6:102;
then A48: ( (1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) is_integrable_on M & (1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) is_integrable_on M ) by MESFUNC6:102;
then A49: ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_integrable_on M by MESFUNC6:100;
A51: dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = dom (f1 (#) g1) by VALUED_1:def 5;
then A52: dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (dom f1) /\ (dom g1) by VALUED_1:def 4;
dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) = dom (abs (f1 (#) g1)) by VALUED_1:def 5;
then A53: dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) = dom (f1 (#) g1) by VALUED_1:def 11;
A54: (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1) is_measurable_on EDf /\ EDg by A14, A15, MESFUNC6:21;
for x being Element of X st x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) holds
abs (((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x) <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x

proof

let x be Element of X; :: thesis: ( x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) implies abs (((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x) <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x )
assume A55: x in dom ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) ; :: thesis: abs (((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x) <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x
( (abs f1) . x >= 0 & (abs g1) . x >= 0 ) by MESFUNC6:51;
then A56: ((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) * ((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) <= ((((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) to_power m) / m) + ((((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) to_power n) / n) by A1, A2, A42, HOLDER_1:5;
dom ((abs f1) (#) (abs g1)) = (dom (abs f1)) /\ (dom (abs g1)) by VALUED_1:def 4;
then A57: ((abs f1) (#) (abs g1)) . x = ((abs f1) . x) * ((abs g1) . x) by A9, A52, A55, VALUED_1:def 4;
A58: ((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) * ((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) = (((1 / (s1 to_power (1 / m))) * (1 / (s2 to_power (1 / n)))) * ((abs f1) . x)) * ((abs g1) . x)
.= ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * ((abs f1) . x)) * ((abs g1) . x) by XCMPLX_1:103
.= (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * (((abs f1) (#) (abs g1)) . x) by A57
.= (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * ((abs (f1 (#) g1)) . x) by RFUNCT_1:36
.= ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1))) . x by A51, A55, A53, VALUED_1:def 5
.= (abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))) . x by A43, RFUNCT_1:37 ;
A59: ( (1 / (s1 to_power (1 / m))) * ((abs f1) . x) = ((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x & (1 / (s2 to_power (1 / n))) * ((abs g1) . x) = ((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x ) by VALUED_1:6;
( dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) = dom f1 & dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) = dom g1 ) by A9, A44, MESFUN6C:def 6;
then ( x in dom (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) & x in dom (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) ) by A52, A55, XBOOLE_0:def 4;
then ( (((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x) to_power m = (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) . x & (((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x) to_power n = (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) . x ) by MESFUN6C:def 6;
then ( ((((1 / (s1 to_power (1 / m))) (#) (abs f1)) . x) to_power m) / m = ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) . x & ((((1 / (s2 to_power (1 / n))) (#) (abs g1)) . x) to_power n) / n = ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) . x ) by VALUED_1:6;
then ((((1 / (s1 to_power (1 / m))) * ((abs f1) . x)) to_power m) / m) + ((((1 / (s2 to_power (1 / n))) * ((abs g1) . x)) to_power n) / n) = (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x by A9, A52, A55, A46, A59, VALUED_1:def 1;
hence abs (((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) . x) <= (((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) . x by A56, A58, VALUED_1:18; :: thesis: verum

end;

then A61: Integral M,(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))) <= Integral M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) by A5, A7, A49, A9, A52, A46, A54, MESFUNC6:96;
A62: ex E1 being Element of S st
( E1 = (dom ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) /\ (dom ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) & Integral M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) = (Integral M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | E1)) + (Integral M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | E1)) ) by A48, MESFUNC6:101;
( EDf = X /\ EDf & EDg = X /\ EDg ) by XBOOLE_1:28;
then A63: ( EDf = X \ Nf & EDg = X \ Ng ) by XBOOLE_1:48;
A64: EDf \ (EDf /\ EDg) = EDf \ EDg by XBOOLE_1:47
.= ((X \ Nf) \ X) \/ ((X \ Nf) /\ Ng) by A63, XBOOLE_1:52
.= (X \ (Nf \/ X)) \/ ((X \ Nf) /\ Ng) by XBOOLE_1:41
.= (X \ X) \/ ((X \ Nf) /\ Ng) by XBOOLE_1:12
.= {} \/ ((X \ Nf) /\ Ng) by XBOOLE_1:37 ;
A65: EDg \ (EDf /\ EDg) = EDg \ EDf by XBOOLE_1:47
.= ((X \ Ng) \ X) \/ ((X \ Ng) /\ Nf) by A63, XBOOLE_1:52
.= (X \ (Ng \/ X)) \/ ((X \ Ng) /\ Nf) by XBOOLE_1:41
.= (X \ X) \/ ((X \ Ng) /\ Nf) by XBOOLE_1:12
.= {} \/ ((X \ Ng) /\ Nf) by XBOOLE_1:37 ;
set NF = EDf /\ Ng;
set NG = EDg /\ Nf;
( Nf is measure_zero of M & Ng is measure_zero of M ) by A5, A7, MEASURE1:def 13;
then ( EDf /\ Ng is measure_zero of M & EDg /\ Nf is measure_zero of M ) by MEASURE1:69, XBOOLE_1:17;
then A66: ( M . (EDf /\ Ng) = 0 & M . (EDg /\ Nf) = 0 ) by MEASURE1:def 13;
( EDf /\ EDg = EDf /\ (EDf /\ EDg) & EDf /\ EDg = EDg /\ (EDf /\ EDg) ) by XBOOLE_1:17, XBOOLE_1:28;
then A67: ( EDf /\ EDg = EDf \ (EDf /\ Ng) & EDf /\ EDg = EDg \ (EDg /\ Nf) ) by A63, A64, A65, XBOOLE_1:48;
R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) is_integrable_on M by A48, MESFUNC6:def 9;
then ex E being Element of S st
( E = dom (R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m))) & R_EAL ((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) is_measurable_on E ) by MESFUNC5:def 17;
then A68: (1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m) is_measurable_on EDf by A45, A9, A5, MESFUNC6:def 6;
R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_integrable_on M by A48, MESFUNC6:def 9;
then ex E being Element of S st
( E = dom (R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) & R_EAL ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) is_measurable_on E ) by MESFUNC5:def 17;
then A69: (1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n) is_measurable_on EDg by A45, A9, A7, MESFUNC6:def 6;
(1 / (s1 to_power (1 / m))) to_power m = (s1 to_power (1 / m)) to_power (- m) by A41, A8, POWER:37, POWER:39;
then (1 / (s1 to_power (1 / m))) to_power m = s1 to_power ((1 / m) * (- m)) by A8, A41, POWER:38;
then (1 / (s1 to_power (1 / m))) to_power m = s1 to_power (- ((1 * (1 / m)) * m)) ;
then (1 / (s1 to_power (1 / m))) to_power m = s1 to_power (- 1) by XCMPLX_1:107;
then (1 / (s1 to_power (1 / m))) to_power m = (1 / s1) to_power 1 by A8, A41, POWER:37;
then A70: (1 / (s1 to_power (1 / m))) to_power m = 1 / s1 by POWER:30;
( (R_EAL (1 / s1)) * (R_EAL s1) = (1 / s1) * s1 & (R_EAL (1 / s2)) * (R_EAL s2) = (1 / s2) * s2 ) by EXTREAL1:38;
then A71: ( (R_EAL (1 / s1)) * (R_EAL s1) = 1 & (R_EAL (1 / s2)) * (R_EAL s2) = 1 ) by A41, XCMPLX_1:107;
A72: (1 / (s2 to_power (1 / n))) to_power n = (s2 to_power (1 / n)) to_power (- n) by A41, A8, POWER:37, POWER:39
.= s2 to_power ((1 / n) * (- n)) by A8, A41, POWER:38
.= s2 to_power (- ((1 * (1 / n)) * n))
.= s2 to_power (- 1) by XCMPLX_1:107
.= (1 / s2) to_power 1 by A8, A41, POWER:37
.= 1 / s2 by POWER:30 ;
A73: Integral M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) | (EDf /\ EDg)) = Integral M,((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) by A5, A9, A45, A67, A66, A68, MESFUNC6:89
.= (R_EAL (1 / m)) * (Integral M,(((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) by A47, MESFUNC6:102
.= (R_EAL (1 / m)) * (Integral M,(((1 / (s1 to_power (1 / m))) to_power m) (#) ((abs f1) to_power m))) by A42, Lm001f
.= (R_EAL (1 / m)) * ((R_EAL ((1 / (s1 to_power (1 / m))) to_power m)) * (Integral M,((abs f1) to_power m))) by A4, MESFUNC6:102
.= 1 / m by A70, A71, XXREAL_3:92 ;
Integral M,(((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) | (EDf /\ EDg)) = Integral M,((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) by A7, A9, A45, A67, A66, A69, MESFUNC6:89
.= (R_EAL (1 / n)) * (Integral M,(((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n)) by A47, MESFUNC6:102
.= (R_EAL (1 / n)) * (Integral M,(((1 / (s2 to_power (1 / n))) to_power n) (#) ((abs g1) to_power n))) by A42, Lm001f
.= (R_EAL (1 / n)) * ((R_EAL ((1 / (s2 to_power (1 / n))) to_power n)) * (Integral M,((abs g1) to_power n))) by A6, MESFUNC6:102
.= 1 / n by A71, A72, XXREAL_3:92 ;
then A75: Integral M,(((1 / m) (#) (((1 / (s1 to_power (1 / m))) (#) (abs f1)) to_power m)) + ((1 / n) (#) (((1 / (s2 to_power (1 / n))) (#) (abs g1)) to_power n))) = 1 by A1, A45, A5, A7, A9, A62, A73, SUPINF_2:1;
abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (abs (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) (#) (abs (f1 (#) g1)) by RFUNCT_1:37;
then abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1)) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (abs (f1 (#) g1)) by A42, ABSVALUE:def 1;
then A76: Integral M,(abs ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) (#) (f1 (#) g1))) = (R_EAL (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * (Integral M,(abs (f1 (#) g1))) by A18, MESFUNC6:102;
reconsider c1 = Integral M,(abs (f1 (#) g1)) as Real by A17, LPSPACE1:44;
(R_EAL (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * (Integral M,(abs (f1 (#) g1))) = (R_EAL (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * (R_EAL c1) ;
then (R_EAL (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * (Integral M,(abs (f1 (#) g1))) = (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1 by EXTREAL1:38;
then ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * ((1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) * c1) <= ((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * 1 by A42, A61, A76, A75, XREAL_1:66;
then A77: (((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n))))) * c1 <= (s1 to_power (1 / m)) * (s2 to_power (1 / n)) ;
((s1 to_power (1 / m)) * (s2 to_power (1 / n))) * (1 / ((s1 to_power (1 / m)) * (s2 to_power (1 / n)))) = 1 by A42, XCMPLX_1:107;
hence ex r1 being Real st
( r1 = Integral M,((abs f) to_power m) & ex r2 being Real st
( r2 = Integral M,((abs g) to_power n) & Integral M,(abs (f (#) g)) <= (r1 to_power (1 / m)) * (r2 to_power (1 / n)) ) ) by A4, A6, A77; :: thesis: verum

end;

end;