set C = CosetSet (M,k);
defpred S₁[ 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 :: thesis: for A, B being Element of CosetSet (M,k) ex z being Element of CosetSet (M,k) st S₁[A,B,z]

let A, B be Element of CosetSet (M,k); :: thesis: ex z being Element of CosetSet (M,k) st S₁[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; :: thesis: S₁[A,B,z]

now :: thesis: 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; :: thesis: ( a1 in A & b1 in B implies z = a.e-eq-class_Lp ((a1 + b1),M,k) )
assume ( a1 in A & b1 in B ) ; :: thesis: 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; :: thesis: verum

end;

hence S₁[A,B,z] ; :: thesis: 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 S₁[A,B,f . (A,B)] from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (CosetSet (M,k)) ;
take f ; :: thesis: 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); :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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; :: thesis: verum