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 :: thesis: for A, B being Element of CosetSet M ex z being Element of CosetSet M st S₁[A,B,z]

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 :: thesis: for a1, b1 being PartFunc of X,REAL st a1 in A & b1 in B holds
z = a.e-eq-class ((a1 + b1),M)

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