let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
let S be SigmaField of X; :: thesis: for M being sigma_Measure of S holds
( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )
let M be sigma_Measure of S; :: thesis: ( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable )

now

let x, y be Point of (L-1-Space M); :: thesis: for a being Real holds
( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
let a be Real; :: thesis: ( ( ||.x.|| = 0 implies x = 0. (L-1-Space M) ) & ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
consider f being PartFunc of X,REAL such that
A1: f in x and
A2: ||.x.|| = Integral M,(abs f) by Def19;
abs f is_integrable_on M by A1, Th48;
then Integral M,((abs a) (#) (abs f)) = (R_EAL (abs a)) * (Integral M,(abs f)) by MESFUNC6:102;
then Integral M,(abs (a (#) f)) = (R_EAL (abs a)) * (Integral M,(abs f)) by RFUNCT_1:37;
then A3: Integral M,(abs (a (#) f)) = (abs a) * ||.x.|| by A2, EXTREAL1:13;

hereby :: thesis: ( ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )

set g = X --> 0 ;
reconsider x1 = x as Point of (Pre-L-Space M) ;
consider f being PartFunc of X,REAL such that
A4: f in x1 and
(L-1-Norm M) . x1 = Integral M,(abs f) by Def19;
A5: f in L1_Functions M by A4, Th48;
then A6: a.e-eq-class f,M in CosetSet M ;
A7: X --> 0 in L1_Functions M by Lm3;
assume ||.x.|| = 0 ; :: thesis: x = 0. (L-1-Space M)
then Integral M,(abs f) = 0 by A4, Th50;
then f a.e.= X --> 0 ,M by A5, Th54;
then a.e-eq-class (X --> 0 ),M = a.e-eq-class f,M by A5, A7, Th39;
then zeroCoset M = a.e-eq-class f,M by A7, A6, Def16;
then 0. (Pre-L-Space M) = a.e-eq-class f,M by Def18;
hence x = 0. (L-1-Space M) by A4, Th51; :: thesis: verum

end;

hereby :: thesis: ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )

reconsider x1 = x as Point of (Pre-L-Space M) ;
consider f being PartFunc of X,REAL such that
A8: f = X --> 0 and
A9: ( f in L1_Functions M & zeroCoset M = a.e-eq-class f,M ) by Def16;
assume x = 0. (L-1-Space M) ; :: thesis: ||.x.|| = 0
then x1 = 0. (Pre-L-Space M) ;
then A10: x1 = zeroCoset M by Def18;
(L-1-Norm M) . x1 = ||.x.|| ;
then (L-1-Norm M) . x1 = Integral M,(abs f) by A10, A9, Th38, Th50;
hence ||.x.|| = 0 by A8, Th55; :: thesis: verum

end;

A11: f is_integrable_on M by A1, Th48;
then |.(Integral M,f).| <= Integral M,(abs f) by MESFUNC6:95;
hence 0 <= ||.x.|| by A2, EXTREAL2:51; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = (abs a) * ||.x.|| )
consider g being PartFunc of X,REAL such that
A12: g in y and
A13: ||.y.|| = Integral M,(abs g) by Def19;
A14: g is_integrable_on M by A12, Th48;
f + g in x + y by A1, A12, Th52;
then A15: ||.(x + y).|| = Integral M,(abs (f + g)) by Th50;
(Integral M,(abs f)) + (Integral M,(abs g)) = ||.x.|| + ||.y.|| by A2, A13, SUPINF_2:1;
hence ||.(x + y).|| <= ||.x.|| + ||.y.|| by A11, A15, A14, Th56; :: thesis: ||.(a * x).|| = (abs a) * ||.x.||
a (#) f in a * x by A1, Th52;
hence ||.(a * x).|| = (abs a) * ||.x.|| by A3, Th50; :: thesis: verum

end;

hence ( L-1-Space M is RealNormSpace-like & L-1-Space M is RealLinearSpace-like & L-1-Space M is Abelian & L-1-Space M is add-associative & L-1-Space M is right_zeroed & L-1-Space M is right_complementable ) by NORMSP_1:def 2, RSSPACE3:4; :: thesis: verum