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);

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 A3, Th38;

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 A6, Th38;

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;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 A3, Th38;

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 A6, Th38;

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

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 A11, Th38;

then (lmultCoset (M,k)) . (a,x) = a.e-eq-class_Lp ((a (#) f1),M,k) by A10, Def10;

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 A9, A11;

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 A11, A9, Th47;

hence a (#) f in a * x by A12, Th26, A9, A11, Th38; :: thesis: verum

end;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 A11, Th38;

then (lmultCoset (M,k)) . (a,x) = a.e-eq-class_Lp ((a (#) f1),M,k) by A10, Def10;

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 A9, A11;

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 A11, A9, Th47;

hence a (#) f in a * x by A12, Th26, A9, A11, Th38; :: thesis: verum