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 VSPDef6X;
then X --> 0 in 0. (Lp-Space M,k) by EQC01, LmDef1Lp;
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 Lm17z;
then consider r0 being Real such that
A14a: ( 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 A14a, Lm262;
hence ||.(0. (Lp-Space M,k)).|| = 0 by A14a, POWER:def 2; :: according to NORMSP_0:def 6 :: thesis:

now

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

hereby :: thesis:

assume A2: ||.x.|| = 0 ; :: thesis:
consider f being PartFunc of X,REAL such that
A3: ( f in x & ex r being Real st
( r = Integral M,((abs f) to_power k) & ||.x.|| = r to_power (1 / k) ) ) by DefLpNORM;
A3a: f in Lp_Functions M,k by Lm16, A3;
then consider r1 being Real such that
A3c: ( r1 = Integral M,((abs f) to_power k) & r1 >= 0 & (Lp-Norm M,k) . x = r1 to_power (1 / k) ) by A3, Lm15;
r1 = 0 by A2, A3c, POWER:39;
then zeroCoset M,k = a.e-eq-class_Lp f,M,k by A3a, A3c, Lm261, EQC02bx;
then 0. (Pre-Lp-Space M,k) = a.e-eq-class_Lp f,M,k by VSPDef6X;
hence x = 0. (Lp-Space M,k) by A3, Lm17z; :: thesis:

end;

consider f being PartFunc of X,REAL such that
A15: ( f in x & ex r1 being Real st
( r1 = Integral M,((abs f) to_power k) & ||.x.|| = r1 to_power (1 / k) ) ) by DefLpNORM;
A15a: ( (abs f) to_power k is_integrable_on M & f in Lp_Functions M,k ) by Lm16, A15;
consider g being PartFunc of X,REAL such that
A16: ( g in y & ex r2 being Real st
( r2 = Integral M,((abs g) to_power k) & ||.y.|| = r2 to_power (1 / k) ) ) by DefLpNORM;
A16a: ( (abs g) to_power k is_integrable_on M & g in Lp_Functions M,k ) by Lm16, A16;
consider s1 being Real such that
A17: ( s1 = Integral M,((abs f) to_power k) & ||.x.|| = s1 to_power (1 / k) ) by A15;
B17: ( s1 = 0 implies s1 to_power (1 / k) >= 0 ) by POWER:def 2;
( s1 > 0 implies s1 to_power (1 / k) >= 0 ) by POWER:39;
hence 0 <= ||.x.|| by B17, A15a, A17, Lm15; :: thesis:
set t = f + g;
set w = x + y;
A17a: s1 >= 0 by A15a, A17, Lm15;
consider s2 being Real such that
A17b: ( s2 = Integral M,((abs g) to_power k) & ||.y.|| = s2 to_power (1 / k) ) by A16;
f + g in x + y by Lm17Y, A15, A16;
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 Lm17x;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by Th002X, ASK, A15a, A16a, A17b, A17; :: thesis:
set t = a (#) f;
set w = a * x;
a (#) f in a * x by Lm17Y, A15;
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 Lm17x;
then consider s being Real such that
A30: ( s = Integral M,((abs (a (#) f)) to_power k) & ||.(a * x).|| = s to_power (1 / k) ) ;
A32: s = Integral M,(((abs a) to_power k) (#) ((abs f) to_power k)) by A30, Lm001e
.= (R_EAL ((abs a) to_power k)) * (R_EAL s1) by A17, A15a, MESFUNC6:102
.= ((abs a) to_power k) * s1 by EXTREAL1:38 ;
(abs a) to_power k >= 0 by LmPW001, COMPLEX1:132;
then ||.(a * x).|| = (((abs a) to_power k) to_power (1 / k)) * (s1 to_power (1 / k)) by A17a, A30, A32, LmPW003
.= ((abs a) to_power (k * (1 / k))) * (s1 to_power (1 / k)) by COMPLEX1:132, HOLDER_1:2
.= ((abs a) to_power 1) * (s1 to_power (1 / k)) by XCMPLX_1:107 ;
hence ||.(a * x).|| = (abs a) * ||.x.|| by A17, POWER:30; :: 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_0:def 5, NORMSP_1:def 2, RSSPACE3:4; :: thesis: