let X be non empty set ; :: thesis:
let S be SigmaField of X; :: thesis:
let M be sigma_Measure of S; :: thesis:
let k be geq_than_1 Real; :: thesis:
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 Th38, Th23;
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 A1, Th58;
hence ||.(0. (Lp-Space (M,k))).|| = 0 by A1, POWER:def 2; :: according to NORMSP_0:def 6 :: thesis:

now :: thesis:

let x, y be Point of (Lp-Space (M,k)); :: thesis:
let a be Real; :: thesis:
A2: 1 <= k by Def1;

hereby :: thesis:

assume A3: ||.x.|| = 0 ; :: thesis:
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)) & ||.x.|| = r to_power (1 / k) ) ) by Def12;
A5: f in Lp_Functions (M,k) by Th51, A4;
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 A4, Th49;
r1 = 0 by A3, A6, POWER:34;
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 A4, Th55; :: thesis:

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)) & ||.x.|| = r1 to_power (1 / k) ) ) by Def12;
A8: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions (M,k) ) by Th51, A7;
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)) & ||.y.|| = r2 to_power (1 / k) ) ) by Def12;
A10: ( (abs g) to_power k is_integrable_on M & g in Lp_Functions (M,k) ) by Th51, A9;
consider s1 being Real such that
A11: ( s1 = Integral (M,((abs f) to_power k)) & ||.x.|| = 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 <= ||.x.|| by A12, A8, A11, Th49; :: thesis:
set t = f + g;
set w = x + y;
A13: s1 >= 0 by A8, A11, Th49;
consider s2 being Real such that
A14: ( s2 = Integral (M,((abs g) to_power k)) & ||.y.|| = 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).|| <= ||.x.|| + ||.y.|| by Th61, A2, A8, A10, A14, A11; :: thesis:
set t = a (#) f;
set w = a * x;
a (#) f in a * x by Th54, A7;
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 A15, Th18
.= r * (Integral (M,((abs f) to_power k))) by A8, MESFUNC6:102
.= r * s1 by A11, EXTREAL1:1
.= (|.a.| to_power k) * s1 ;
|.a.| to_power k >= 0 by Th4, COMPLEX1:46;
then ||.(a * x).|| = ((|.a.| to_power k) 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 COMPLEX1:46, HOLDER_1:2
.= (|.a.| to_power 1) * (s1 to_power (1 / k)) by XCMPLX_1:106 ;
hence ||.(a * x).|| = |.a.| * ||.x.|| by A11, POWER:25; :: thesis:

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 NORMSP_1:def 1, RSSPACE3:2; :: thesis: