set C = CosetSet (M,k);
defpred S1[ Real, set , set ] means for f being PartFunc of X,REAL st f in $2 holds
$3 = a.e-eq-class_Lp (($1 (#) f),M,k);
A1:
now for z being Element of REAL
for A being Element of CosetSet (M,k) ex c being Element of CosetSet (M,k) st S1[z,A,c]let z be
Element of
REAL ;
for A being Element of CosetSet (M,k) ex c being Element of CosetSet (M,k) st S1[z,A,c]let A be
Element of
CosetSet (
M,
k);
ex c being Element of CosetSet (M,k) st S1[z,A,c]
A in CosetSet (
M,
k)
;
then consider a being
PartFunc of
X,
REAL such that A2:
(
A = a.e-eq-class_Lp (
a,
M,
k) &
a in Lp_Functions (
M,
k) )
;
A3:
ex
E being
Element of
S st
(
M . (E `) = 0 &
E = dom a &
a is
E -measurable )
by A2, Th35;
set c =
a.e-eq-class_Lp (
(z (#) a),
M,
k);
z (#) a in Lp_Functions (
M,
k)
by Th26, A2;
then
a.e-eq-class_Lp (
(z (#) a),
M,
k)
in CosetSet (
M,
k)
;
then reconsider c =
a.e-eq-class_Lp (
(z (#) a),
M,
k) as
Element of
CosetSet (
M,
k) ;
take c =
c;
S1[z,A,c]now for a1 being PartFunc of X,REAL st a1 in A holds
c = a.e-eq-class_Lp ((z (#) a1),M,k)let a1 be
PartFunc of
X,
REAL;
( a1 in A implies c = a.e-eq-class_Lp ((z (#) a1),M,k) )assume
a1 in A
;
c = a.e-eq-class_Lp ((z (#) a1),M,k)then
z (#) a1 a.e.= z (#) a,
M
by A2, A3, Th37, LPSPACE1:32;
hence
c = a.e-eq-class_Lp (
(z (#) a1),
M,
k)
by Th42;
verum end; hence
S1[
z,
A,
c]
;
verum end;
consider f being Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)) such that
A4:
for z being Element of REAL
for A being Element of CosetSet (M,k) holds S1[z,A,f . (z,A)]
from BINOP_1:sch 3(A1);
A5:
for z being Real
for A being Element of CosetSet (M,k) holds S1[z,A,f . (z,A)]
proof
let z be
Real;
for A being Element of CosetSet (M,k) holds S1[z,A,f . (z,A)]let A be
Element of
CosetSet (
M,
k);
S1[z,A,f . (z,A)]
reconsider z =
z as
Element of
REAL by XREAL_0:def 1;
S1[
z,
A,
f . (
z,
A)]
by A4;
hence
S1[
z,
A,
f . (
z,
A)]
;
verum
end;
take
f
; for z being Real
for A being Element of CosetSet (M,k)
for f being PartFunc of X,REAL st f in A holds
f . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k)
let z be Real; for A being Element of CosetSet (M,k)
for f being PartFunc of X,REAL st f in A holds
f . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k)
let A be Element of CosetSet (M,k); for f being PartFunc of X,REAL st f in A holds
f . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k)
let a be PartFunc of X,REAL; ( a in A implies f . (z,A) = a.e-eq-class_Lp ((z (#) a),M,k) )
assume
a in A
; f . (z,A) = a.e-eq-class_Lp ((z (#) a),M,k)
hence
f . (z,A) = a.e-eq-class_Lp ((z (#) a),M,k)
by A5; verum