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 vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & 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 vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & 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 vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & 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 :: thesis: for x, y being Point of (L-1-Space M)
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).|| = |.a.| * ||.x.|| )

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).|| = |.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).|| = |.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, Th47;
then Integral (M,(|.a.| (#) (abs f))) = |.a.| * (Integral (M,(abs f))) by MESFUNC6:102;
then Integral (M,(abs (a (#) f))) = |.a.| * (Integral (M,(abs f))) by RFUNCT_1:25;
then A3: Integral (M,(abs (a (#) f))) = |.a.| * ||.x.|| by A2, EXTREAL1:1;

hereby :: thesis: ( ( x = 0. (L-1-Space M) implies ||.x.|| = 0 ) & 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.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, Th47;
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, Th49;
then f a.e.= X --> 0,M by A5, Th53;
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, Th50; :: thesis: verum

end;

hereby :: thesis: ( 0 <= ||.x.|| & ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.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, Th49;
hence ||.x.|| = 0 by A8, Th54; :: thesis: verum

end;

A11: f is_integrable_on M by A1, Th47;
then |.(Integral (M,f)).| <= Integral (M,(abs f)) by MESFUNC6:95;
hence 0 <= ||.x.|| by A2, EXTREAL1:14; :: thesis: ( ||.(x + y).|| <= ||.x.|| + ||.y.|| & ||.(a * x).|| = |.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, Th47;
f + g in x + y by A1, A12, Th51;
then A15: ||.(x + y).|| = Integral (M,(abs (f + g))) by Th49;
(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, Th55; :: thesis: ||.(a * x).|| = |.a.| * ||.x.||
a (#) f in a * x by A1, Th51;
hence ||.(a * x).|| = |.a.| * ||.x.|| by A3, Th49; :: thesis: verum

end;

hence ( L-1-Space M is RealNormSpace-like & L-1-Space M is vector-distributive & L-1-Space M is scalar-distributive & L-1-Space M is scalar-associative & L-1-Space M is scalar-unital & 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 1, RSSPACE3:2; :: thesis: verum