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 (a + b),M;
set C = CosetSet M;

A1: now

let A, B be Element of CosetSet M; :: thesis: ex z being Element of CosetSet M st S₁[A,B,z]
A in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A2: A = a.e-eq-class a,M and
A3: a in L1_Functions M ;
B in CosetSet M ;
then consider b being PartFunc of X,REAL such that
A4: B = a.e-eq-class b,M and
A5: b in L1_Functions M ;
set z = a.e-eq-class (a + b),M;
A6: a + b in L1_Functions M by A3, A5, Th23;
then a.e-eq-class (a + b),M in CosetSet M ;
then reconsider z = a.e-eq-class (a + b),M as Element of CosetSet M ;
take z = z; :: thesis: S₁[A,B,z]

now

let a1, b1 be PartFunc of X,REAL ; :: thesis: ( a1 in A & b1 in B implies z = a.e-eq-class (a1 + b1),M )
assume A7: ( a1 in A & b1 in B ) ; :: thesis: z = a.e-eq-class (a1 + b1),M
then ( a1 a.e.= a,M & b1 a.e.= b,M ) by A2, A3, A4, A5, Th37;
then A8: a1 + b1 a.e.= a + b,M by Th31;
a1 + b1 in L1_Functions M by A7, Th23;
hence z = a.e-eq-class (a1 + b1),M by A6, A8, Th39; :: thesis: verum

end;

hence S₁[A,B,z] ; :: thesis: verum

end;

consider f being Function of [:(CosetSet M),(CosetSet M):],(CosetSet M) such that
A9: for A, B being Element of CosetSet M holds S₁[A,B,f . A,B] from BINOP_1:sch 3(A1);
reconsider f = f as BinOp of (CosetSet M) ;
take f ; :: thesis: for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f . A,B = a.e-eq-class (a + b),M
let A, B be Element of CosetSet M; :: thesis: for a, b being PartFunc of X,REAL st a in A & b in B holds
f . A,B = a.e-eq-class (a + b),M
let a, b be PartFunc of X,REAL ; :: thesis: ( a in A & b in B implies f . A,B = a.e-eq-class (a + b),M )
assume ( a in A & b in B ) ; :: thesis: f . A,B = a.e-eq-class (a + b),M
hence f . A,B = a.e-eq-class (a + b),M by A9; :: thesis: verum