set C = CosetSet M,k;
defpred S1[ set , set , set ] means for a, b being PartFunc of X,REAL st a in $1 & b in $2 holds
$3 = a.e-eq-class_Lp (a + b),M,k;
A1:
now let A,
B be
Element of
CosetSet M,
k;
ex z being Element of CosetSet M,k st S1[A,B,z]
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 )
;
B2:
ex
E being
Element of
S st
(
M . (E ` ) = 0 &
dom a = E &
a is_measurable_on E )
by A2, EQC00a;
B in CosetSet M,
k
;
then consider b being
PartFunc of
X,
REAL such that A3:
(
B = a.e-eq-class_Lp b,
M,
k &
b in Lp_Functions M,
k )
;
B3:
ex
E being
Element of
S st
(
M . (E ` ) = 0 &
dom b = E &
b is_measurable_on E )
by A3, EQC00a;
set z =
a.e-eq-class_Lp (a + b),
M,
k;
a + b in Lp_Functions M,
k
by Th01aLp, A2, A3;
then
a.e-eq-class_Lp (a + b),
M,
k in CosetSet M,
k
;
then reconsider z =
a.e-eq-class_Lp (a + b),
M,
k as
Element of
CosetSet M,
k ;
take z =
z;
S1[A,B,z]now let a1,
b1 be
PartFunc of
X,
REAL ;
( a1 in A & b1 in B implies z = a.e-eq-class_Lp (a1 + b1),M,k )assume
(
a1 in A &
b1 in B )
;
z = a.e-eq-class_Lp (a1 + b1),M,kthen
(
a1 a.e.= a,
M &
b1 a.e.= b,
M )
by A2, B2, A3, B3, EQC00c;
hence
z = a.e-eq-class_Lp (a1 + b1),
M,
k
by EQC02bx, LPSPACE1:31;
verum end; hence
S1[
A,
B,
z]
;
verum end;
consider f being Function of [:(CosetSet M,k),(CosetSet M,k):],(CosetSet M,k) such that
A8:
for A, B being Element of CosetSet M,k holds S1[A,B,f . A,B]
from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (CosetSet M,k) ;
take
f
; for A, B being Element of CosetSet M,k
for a, b being PartFunc of X,REAL st a in A & b in B holds
f . A,B = a.e-eq-class_Lp (a + b),M,k
let A, B be Element of CosetSet M,k; for a, b being PartFunc of X,REAL st a in A & b in B holds
f . A,B = a.e-eq-class_Lp (a + b),M,k
let a, b be PartFunc of X,REAL ; ( a in A & b in B implies f . A,B = a.e-eq-class_Lp (a + b),M,k )
assume
( a in A & b in B )
; f . A,B = a.e-eq-class_Lp (a + b),M,k
hence
f . A,B = a.e-eq-class_Lp (a + b),M,k
by A8; verum