let X be non empty set ; :: thesis: for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

let S be SigmaField of X; :: thesis: for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

let M be sigma_Measure of S; :: thesis: for f, g being PartFunc of X,REAL
for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

let f, g be PartFunc of X,REAL; :: thesis: for a being Real
for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

let a be Real; :: thesis: for k being positive Real
for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

let k be positive Real; :: thesis: for x, y being Point of (Lp-Space (M,k)) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )

let x, y be Point of (Lp-Space (M,k)); :: thesis: ( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
set C = CosetSet (M,k);
hereby :: thesis: ( f in x implies a (#) f in a * x )
assume A1: ( f in x & g in y ) ; :: thesis: f + g in x + y
x in the carrier of (Pre-Lp-Space (M,k)) ;
then A2: x in CosetSet (M,k) by Def11;
then consider a being PartFunc of X,REAL such that
A3: ( x = a.e-eq-class_Lp (a,M,k) & a in Lp_Functions (M,k) ) ;
A4: a in x by ;
y in the carrier of (Pre-Lp-Space (M,k)) ;
then A5: y in CosetSet (M,k) by Def11;
then consider b being PartFunc of X,REAL such that
A6: ( y = a.e-eq-class_Lp (b,M,k) & b in Lp_Functions (M,k) ) ;
b in y by ;
then (addCoset (M,k)) . (x,y) = a.e-eq-class_Lp ((a + b),M,k) by A2, A5, A4, Def8;
then A7: x + y = a.e-eq-class_Lp ((a + b),M,k) by Def11;
ex r being PartFunc of X,REAL st
( f = r & r in Lp_Functions (M,k) & a a.e.= r,M ) by A1, A3;
then A8: a.e-eq-class_Lp (a,M,k) = a.e-eq-class_Lp (f,M,k) by Th42;
ex r being PartFunc of X,REAL st
( g = r & r in Lp_Functions (M,k) & b a.e.= r,M ) by A1, A6;
then a.e-eq-class_Lp (b,M,k) = a.e-eq-class_Lp (g,M,k) by Th42;
then a.e-eq-class_Lp ((a + b),M,k) = a.e-eq-class_Lp ((f + g),M,k) by A1, A3, A6, A8, Th45;
hence f + g in x + y by Th38, A7, Th25, A3, A1, A6; :: thesis: verum
end;
hereby :: thesis: verum
assume A9: f in x ; :: thesis: a (#) f in a * x
x in the carrier of (Pre-Lp-Space (M,k)) ;
then A10: x in CosetSet (M,k) by Def11;
then consider f1 being PartFunc of X,REAL such that
A11: ( x = a.e-eq-class_Lp (f1,M,k) & f1 in Lp_Functions (M,k) ) ;
f1 in x by ;
then (lmultCoset (M,k)) . (a,x) = a.e-eq-class_Lp ((a (#) f1),M,k) by ;
then A12: a * x = a.e-eq-class_Lp ((a (#) f1),M,k) by Def11;
ex r being PartFunc of X,REAL st
( f = r & r in Lp_Functions (M,k) & f1 a.e.= r,M ) by ;
then a.e-eq-class_Lp (f1,M,k) = a.e-eq-class_Lp (f,M,k) by Th42;
then a.e-eq-class_Lp ((a (#) f1),M,k) = a.e-eq-class_Lp ((a (#) f),M,k) by ;
hence a (#) f in a * x by A12, Th26, A9, A11, Th38; :: thesis: verum
end;