let a be Real; :: 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,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 ; :: thesis: 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; :: thesis: 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; :: thesis: 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 ; :: thesis: 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); :: 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;
hereby :: thesis: ( f in x implies a (#) f in a * x )
assume A2:
(
f in x &
g in y )
;
:: thesis: f + g in x + yreconsider x1 =
x,
y1 =
y as
Point of
(Pre-L-Space M) ;
x1 in the
carrier of
(Pre-L-Space M)
;
then A3:
x1 in CosetSet M
by VSPDef6X;
then consider a being
PartFunc of
X,
REAL such that A4:
(
x1 = a.e-eq-class a,
M &
a in L1_Functions M )
;
A5:
a in x1
by A4, EQC01;
y1 in the
carrier of
(Pre-L-Space M)
;
then A6:
y1 in CosetSet M
by VSPDef6X;
then consider b being
PartFunc of
X,
REAL such that A7:
(
y1 = a.e-eq-class b,
M &
b in L1_Functions M )
;
b in y1
by A7, EQC01;
then
(addCoset M) . x1,
y1 = a.e-eq-class (a + b),
M
by A3, A6, A5, VSPDef3X;
then A9:
x1 + y1 = a.e-eq-class (a + b),
M
by VSPDef6X;
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 A2, A4;
then A11:
a.e-eq-class a,
M = a.e-eq-class f,
M
by EQC02;
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, A7;
then
a.e-eq-class b,
M = a.e-eq-class g,
M
by EQC02;
then
a.e-eq-class (a + b),
M = a.e-eq-class (f + g),
M
by A2, A4, A7, A11, EQC03;
hence
f + g in x + y
by EQC01, A9, Th01a, A4, A2, A7;
:: thesis: verum
end;
hereby :: thesis: verum
assume A15:
f in x
;
:: thesis: a (#) f in a * xreconsider x1 =
x as
Point of
(Pre-L-Space M) ;
x1 in the
carrier of
(Pre-L-Space M)
;
then A16:
x1 in CosetSet M
by VSPDef6X;
then consider f1 being
PartFunc of
X,
REAL such that A17:
(
x1 = a.e-eq-class f1,
M &
f1 in L1_Functions M )
;
f1 in x1
by A17, EQC01;
then
(lmultCoset M) . a,
x1 = a.e-eq-class (a (#) f1),
M
by A16, VSPDef5X;
then A19:
a * x1 = a.e-eq-class (a (#) f1),
M
by VSPDef6X;
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 A15, A17;
then
a.e-eq-class f1,
M = a.e-eq-class f,
M
by EQC02;
then
a.e-eq-class (a (#) f1),
M = a.e-eq-class (a (#) f),
M
by A17, A15, EQC04;
hence
a (#) f in a * x
by A19, Th01b, A15, A17, EQC01;
:: thesis: verum
end;