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 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; 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; 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 ; 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; 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; 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); ( ( 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 ( f in x implies a (#) f in a * x )
assume A2:
(
f in x &
g in y )
;
f + g in x + y
x in the
carrier of
(Pre-Lp-Space M,k)
;
then A3:
x in CosetSet M,
k
by VSPDef6X;
then consider a being
PartFunc of
X,
REAL such that A4:
(
x = a.e-eq-class_Lp a,
M,
k &
a in Lp_Functions M,
k )
;
A5:
a in x
by A4, EQC01;
y in the
carrier of
(Pre-Lp-Space M,k)
;
then A6:
y in CosetSet M,
k
by VSPDef6X;
then consider b being
PartFunc of
X,
REAL such that A7:
(
y = a.e-eq-class_Lp b,
M,
k &
b in Lp_Functions M,
k )
;
b in y
by A7, EQC01;
then
(addCoset M,k) . x,
y = a.e-eq-class_Lp (a + b),
M,
k
by A3, A6, A5, VSPDef3X;
then A9:
x + y = a.e-eq-class_Lp (a + b),
M,
k
by VSPDef6X;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in Lp_Functions M,
k &
a a.e.= r,
M )
by A2, A4;
then A11:
a.e-eq-class_Lp a,
M,
k = a.e-eq-class_Lp f,
M,
k
by EQC02bx;
ex
r being
PartFunc of
X,
REAL st
(
g = r &
r in Lp_Functions M,
k &
b a.e.= r,
M )
by A2, A7;
then
a.e-eq-class_Lp b,
M,
k = a.e-eq-class_Lp g,
M,
k
by EQC02bx;
then
a.e-eq-class_Lp (a + b),
M,
k = a.e-eq-class_Lp (f + g),
M,
k
by A2, A4, A7, A11, EQC03b;
hence
f + g in x + y
by EQC01, A9, Th01aLp, A4, A2, A7;
verum
end;
hereby verum
assume A15:
f in x
;
a (#) f in a * x
x in the
carrier of
(Pre-Lp-Space M,k)
;
then A16:
x in CosetSet M,
k
by VSPDef6X;
then consider f1 being
PartFunc of
X,
REAL such that A17:
(
x = a.e-eq-class_Lp f1,
M,
k &
f1 in Lp_Functions M,
k )
;
f1 in x
by A17, EQC01;
then
(lmultCoset M,k) . a,
x = a.e-eq-class_Lp (a (#) f1),
M,
k
by A16, VSPDef5X;
then A19:
a * x = a.e-eq-class_Lp (a (#) f1),
M,
k
by VSPDef6X;
ex
r being
PartFunc of
X,
REAL st
(
f = r &
r in Lp_Functions M,
k &
f1 a.e.= r,
M )
by A15, A17;
then
a.e-eq-class_Lp f1,
M,
k = a.e-eq-class_Lp f,
M,
k
by EQC02bx;
then
a.e-eq-class_Lp (a (#) f1),
M,
k = a.e-eq-class_Lp (a (#) f),
M,
k
by A17, A15, EQC04b;
hence
a (#) f in a * x
by A19, Th01bLp, A15, A17, EQC01;
verum
end;