let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for k being geq_than_1 Real holds
( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for k being geq_than_1 Real holds
( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let M be sigma_Measure of S; :: thesis: for k being geq_than_1 Real holds
( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )

let k be geq_than_1 Real; :: thesis: ( Lp-Space (M,k) is reflexive & Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )
set x = 0. (Lp-Space (M,k));
0. (Lp-Space (M,k)) = 0. (Pre-Lp-Space (M,k)) ;
then 0. (Lp-Space (M,k)) = zeroCoset (M,k) by Def11;
then X --> 0 in 0. (Lp-Space (M,k)) by ;
then ex r being Real st
( 0 <= r & r = Integral (M,((abs (X --> 0)) to_power k)) & ||.(0. (Lp-Space (M,k))).|| = r to_power (1 / k) ) by Th55;
then consider r0 being Real such that
A1: ( r0 = Integral (M,((abs (X --> 0)) to_power k)) & (Lp-Norm (M,k)) . (0. (Lp-Space (M,k))) = r0 to_power (1 / k) ) ;
r0 = 0 by ;
hence ||.(0. (Lp-Space (M,k))).|| = 0 by ; :: according to NORMSP_0:def 6 :: thesis: ( Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable )
now :: thesis: for x, y being Point of (Lp-Space (M,k))
for a being Real holds
( ( = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
let x, y be Point of (Lp-Space (M,k)); :: thesis: for a being Real holds
( ( = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )

let a be Real; :: thesis: ( ( = 0 implies x = 0. (Lp-Space (M,k)) ) & 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
A2: 1 <= k by Def1;
hereby :: thesis: ( 0 <= & ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
assume A3: ||.x.|| = 0 ; :: thesis: x = 0. (Lp-Space (M,k))
consider f being PartFunc of X,REAL such that
A4: ( f in x & ex r being Real st
( r = Integral (M,((abs f) to_power k)) & = r to_power (1 / k) ) ) by Def12;
A5: f in Lp_Functions (M,k) by ;
then consider r1 being Real such that
A6: ( r1 = Integral (M,((abs f) to_power k)) & r1 >= 0 & (Lp-Norm (M,k)) . x = r1 to_power (1 / k) ) by ;
r1 = 0 by ;
then zeroCoset (M,k) = a.e-eq-class_Lp (f,M,k) by A5, A6, Th57, Th42;
then 0. (Pre-Lp-Space (M,k)) = a.e-eq-class_Lp (f,M,k) by Def11;
hence x = 0. (Lp-Space (M,k)) by ; :: thesis: verum
end;
consider f being PartFunc of X,REAL such that
A7: ( f in x & ex r1 being Real st
( r1 = Integral (M,((abs f) to_power k)) & = r1 to_power (1 / k) ) ) by Def12;
A8: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) by ;
consider g being PartFunc of X,REAL such that
A9: ( g in y & ex r2 being Real st
( r2 = Integral (M,((abs g) to_power k)) & = r2 to_power (1 / k) ) ) by Def12;
A10: ( (abs g) to_power k is_integrable_on M & g in Lp_Functions (M,k) ) by ;
consider s1 being Real such that
A11: ( s1 = Integral (M,((abs f) to_power k)) & = s1 to_power (1 / k) ) by A7;
A12: ( s1 = 0 implies s1 to_power (1 / k) >= 0 ) by POWER:def 2;
( s1 > 0 implies s1 to_power (1 / k) >= 0 ) by POWER:34;
hence 0 <= by A12, A8, A11, Th49; :: thesis: ( ||.(x + y).|| <= + & ||.(a * x).|| = |.a.| * )
set t = f + g;
set w = x + y;
A13: s1 >= 0 by ;
consider s2 being Real such that
A14: ( s2 = Integral (M,((abs g) to_power k)) & = s2 to_power (1 / k) ) by A9;
f + g in x + y by Th54, A7, A9;
then ex r being Real st
( 0 <= r & r = Integral (M,((abs (f + g)) to_power k)) & ||.(x + y).|| = r to_power (1 / k) ) by Th53;
hence ||.(x + y).|| <= + by Th61, A2, A8, A10, A14, A11; :: thesis: ||.(a * x).|| = |.a.| *
set t = a (#) f;
set w = a * x;
a (#) f in a * x by ;
then ex r being Real st
( 0 <= r & r = Integral (M,((abs (a (#) f)) to_power k)) & ||.(a * x).|| = r to_power (1 / k) ) by Th53;
then consider s being Real such that
A15: ( s = Integral (M,((abs (a (#) f)) to_power k)) & ||.(a * x).|| = s to_power (1 / k) ) ;
reconsider r = |.a.| to_power k as Real ;
A16: s = Integral (M,(r (#) ((abs f) to_power k))) by
.= r * (Integral (M,((abs f) to_power k))) by
.= r * s1 by
.= () * s1 ;
|.a.| to_power k >= 0 by ;
then ||.(a * x).|| = (() to_power (1 / k)) * (s1 to_power (1 / k)) by A13, A15, A16, Th5
.= (|.a.| to_power (k * (1 / k))) * (s1 to_power (1 / k)) by
.= () * (s1 to_power (1 / k)) by XCMPLX_1:106 ;
hence ||.(a * x).|| = |.a.| * by ; :: thesis: verum
end;
hence ( Lp-Space (M,k) is discerning & Lp-Space (M,k) is RealNormSpace-like & Lp-Space (M,k) is vector-distributive & Lp-Space (M,k) is scalar-distributive & Lp-Space (M,k) is scalar-associative & Lp-Space (M,k) is scalar-unital & Lp-Space (M,k) is Abelian & Lp-Space (M,k) is add-associative & Lp-Space (M,k) is right_zeroed & Lp-Space (M,k) is right_complementable ) by ; :: thesis: verum