let a be Complex; :: thesis: for X being non empty set
for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,COMPLEX
for x, y being Point of (L-1-CSpace M) holds
( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
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,COMPLEX
for x, y being Point of (L-1-CSpace M) 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,COMPLEX
for x, y being Point of (L-1-CSpace M) 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,COMPLEX
for x, y being Point of (L-1-CSpace M) 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,COMPLEX; :: thesis: for x, y being Point of (L-1-CSpace M) 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 (L-1-CSpace M); :: thesis: ( ( f in x & g in y implies f + g in x + y ) & ( f in x implies a (#) f in a * x ) )
set C = CCosetSet M;

hereby :: thesis: ( f in x implies a (#) f in a * x )

reconsider x1 = x, y1 = y as Point of (Pre-L-CSpace M) ;
assume that
A1: f in x and
A2: g in y ; :: thesis: f + g in x + y
y1 in the carrier of (Pre-L-CSpace M) ;
then A3: y1 in CCosetSet M by Def19;
then consider b being PartFunc of X,COMPLEX such that
A4: y1 = a.e-Ceq-class (b,M) and
A5: b in L1_CFunctions M ;
A6: b in y1 by A4, A5, Th31;
ex r being PartFunc of X,COMPLEX st
( g = r & r in L1_CFunctions M & b in L1_CFunctions M & b a.e.cpfunc= r,M ) by A2, A4;
then A7: a.e-Ceq-class (b,M) = a.e-Ceq-class (g,M) by Th32;
x1 in the carrier of (Pre-L-CSpace M) ;
then A8: x1 in CCosetSet M by Def19;
then consider a being PartFunc of X,COMPLEX such that
A9: x1 = a.e-Ceq-class (a,M) and
A10: a in L1_CFunctions M ;
a in x1 by A9, A10, Th31;
then (addCCoset M) . (x1,y1) = a.e-Ceq-class ((a + b),M) by A8, A3, A6, Def16;
then A11: x1 + y1 = a.e-Ceq-class ((a + b),M) by Def19;
ex r being PartFunc of X,COMPLEX st
( f = r & r in L1_CFunctions M & a in L1_CFunctions M & a a.e.cpfunc= r,M ) by A1, A9;
then a.e-Ceq-class (a,M) = a.e-Ceq-class (f,M) by Th32;
then a.e-Ceq-class ((a + b),M) = a.e-Ceq-class ((f + g),M) by A1, A2, A9, A10, A4, A5, A7, Th34;
hence f + g in x + y by A1, A2, A9, A4, A11, Th17, Th31; :: thesis: verum

end;

hereby :: thesis: verum

reconsider x1 = x as Point of (Pre-L-CSpace M) ;
x1 in the carrier of (Pre-L-CSpace M) ;
then A12: x1 in CCosetSet M by Def19;
then consider f1 being PartFunc of X,COMPLEX such that
A13: x1 = a.e-Ceq-class (f1,M) and
A14: f1 in L1_CFunctions M ;
(lmultCCoset M) . (a,x1) = a.e-Ceq-class ((a (#) f1),M) by A13, A14, Th31, A12, Def18;
then A15: a * x1 = a.e-Ceq-class ((a (#) f1),M) by Def19;
assume A16: f in x ; :: thesis: a (#) f in a * x
then ex r being PartFunc of X,COMPLEX st
( f = r & r in L1_CFunctions M & f1 in L1_CFunctions M & f1 a.e.cpfunc= r,M ) by A13;
then a.e-Ceq-class (f1,M) = a.e-Ceq-class (f,M) by Th32;
then a.e-Ceq-class ((a (#) f1),M) = a.e-Ceq-class ((a (#) f),M) by A16, A13, A14, Th35;
hence a (#) f in a * x by A16, A13, A15, Th18, Th31; :: thesis: verum

end;