let X be non empty set ; for S being SigmaField of X
for M being sigma_Measure of S holds lmultCoset M = lmultCoset (M,1)
let S be SigmaField of X; for M being sigma_Measure of S holds lmultCoset M = lmultCoset (M,1)
let M be sigma_Measure of S; lmultCoset M = lmultCoset (M,1)
A1:
CosetSet M = CosetSet (M,1)
by Th71;
now for z being Element of REAL
for A being Element of CosetSet M holds (lmultCoset M) . (z,A) = (lmultCoset (M,1)) . (z,A)let z be
Element of
REAL ;
for A being Element of CosetSet M holds (lmultCoset M) . (z,A) = (lmultCoset (M,1)) . (z,A)let A be
Element of
CosetSet M;
(lmultCoset M) . (z,A) = (lmultCoset (M,1)) . (z,A)
A in { (a.e-eq-class (f,M)) where f is PartFunc of X,REAL : f in L1_Functions M }
;
then consider a being
PartFunc of
X,
REAL such that A2:
(
A = a.e-eq-class (
a,
M) &
a in L1_Functions M )
;
A3:
A is
Element of
CosetSet (
M,1)
by Th71;
A4:
a in A
by A2, LPSPACE1:38;
then A5:
(lmultCoset M) . (
z,
A)
= a.e-eq-class (
(z (#) a),
M)
by LPSPACE1:def 17;
z (#) a in L1_Functions M
by A2, LPSPACE1:24;
then
ex
E being
Element of
S st
(
M . (E `) = 0 &
E = dom (z (#) a) &
z (#) a is
E -measurable )
by Lm8;
then
(lmultCoset M) . (
z,
A)
= a.e-eq-class_Lp (
(z (#) a),
M,1)
by A5, Lm12;
hence
(lmultCoset M) . (
z,
A)
= (lmultCoset (M,1)) . (
z,
A)
by A3, A4, Def10;
verum end;
hence
lmultCoset M = lmultCoset (M,1)
by A1, BINOP_1:2; verum