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 for A, B being Element of CosetSet (M,k) ex z being Element of CosetSet (M,k) st S1[A,B,z]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) )
;
A3:
ex
E being
Element of
S st
(
M . (E `) = 0 &
dom a = E &
a is
E -measurable )
by A2, Th35;
B in CosetSet (
M,
k)
;
then consider b being
PartFunc of
X,
REAL such that A4:
(
B = a.e-eq-class_Lp (
b,
M,
k) &
b in Lp_Functions (
M,
k) )
;
A5:
ex
E being
Element of
S st
(
M . (E `) = 0 &
dom b = E &
b is
E -measurable )
by A4, Th35;
set z =
a.e-eq-class_Lp (
(a + b),
M,
k);
a + b in Lp_Functions (
M,
k)
by Th25, A2, A4;
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 for a1, b1 being PartFunc of X,REAL st a1 in A & b1 in B holds
z = a.e-eq-class_Lp ((a1 + b1),M,k)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,k)then
(
a1 a.e.= a,
M &
b1 a.e.= b,
M )
by A2, A3, A4, A5, Th37;
hence
z = a.e-eq-class_Lp (
(a1 + b1),
M,
k)
by Th42, 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
A6:
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 A6; verum