let a be Real; 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,REAL
for x, y being Point of (L-1-Space 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 ; for S being SigmaField of X
for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space 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; for M being sigma_Measure of S
for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space 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; for f, g being PartFunc of X,REAL
for x, y being Point of (L-1-Space 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,REAL; for x, y being Point of (L-1-Space 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-Space M); ( ( 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;
hereby ( f in x implies a (#) f in a * x )
reconsider x1 =
x,
y1 =
y as
Point of
(Pre-L-Space M) ;
assume that A1:
f in x
and A2:
g in y
;
f + g in x + y
y1 in the
carrier of
(Pre-L-Space M)
;
then A3:
y1 in CosetSet M
by Def18;
then consider b being
PartFunc of
X,
REAL such that A4:
y1 = a.e-eq-class (
b,
M)
and A5:
b in L1_Functions M
;
A6:
b in y1
by A4, A5, Th38;
ex
r being
PartFunc of
X,
REAL st
(
g = r &
r in L1_Functions M &
b in L1_Functions M &
b a.e.= r,
M )
by A2, A4;
then A7:
a.e-eq-class (
b,
M)
= a.e-eq-class (
g,
M)
by Th39;
x1 in the
carrier of
(Pre-L-Space M)
;
then A8:
x1 in CosetSet M
by Def18;
then consider a being
PartFunc of
X,
REAL such that A9:
x1 = a.e-eq-class (
a,
M)
and A10:
a in L1_Functions M
;
a in x1
by A9, A10, Th38;
then
(addCoset M) . (
x1,
y1)
= a.e-eq-class (
(a + b),
M)
by A8, A3, A6, Def15;
then A11:
x1 + y1 = a.e-eq-class (
(a + b),
M)
by Def18;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in L1_Functions M &
a in L1_Functions M &
a a.e.= r,
M )
by A1, A9;
then
a.e-eq-class (
a,
M)
= a.e-eq-class (
f,
M)
by Th39;
then
a.e-eq-class (
(a + b),
M)
= a.e-eq-class (
(f + g),
M)
by A1, A2, A9, A10, A4, A5, A7, Th41;
hence
f + g in x + y
by A1, A2, A9, A4, A11, Th23, Th38;
verum
end;
hereby verum
reconsider x1 =
x as
Point of
(Pre-L-Space M) ;
x1 in the
carrier of
(Pre-L-Space M)
;
then A12:
x1 in CosetSet M
by Def18;
then consider f1 being
PartFunc of
X,
REAL such that A13:
x1 = a.e-eq-class (
f1,
M)
and A14:
f1 in L1_Functions M
;
f1 in x1
by A13, A14, Th38;
then
(lmultCoset M) . (
a,
x1)
= a.e-eq-class (
(a (#) f1),
M)
by A12, Def17;
then A15:
a * x1 = a.e-eq-class (
(a (#) f1),
M)
by Def18;
assume A16:
f in x
;
a (#) f in a * xthen
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in L1_Functions M &
f1 in L1_Functions M &
f1 a.e.= r,
M )
by A13;
then
a.e-eq-class (
f1,
M)
= a.e-eq-class (
f,
M)
by Th39;
then
a.e-eq-class (
(a (#) f1),
M)
= a.e-eq-class (
(a (#) f),
M)
by A16, A13, A14, Th42;
hence
a (#) f in a * x
by A16, A13, A15, Th24, Th38;
verum
end;