set C = CosetSet M;
let f1, f2 be BinOp of (CosetSet M); :: 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
f1 . A,B = a.e-eq-class (a + b),M ) & ( for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f2 . A,B = a.e-eq-class (a + b),M ) implies f1 = f2 )
assume that
A10: for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f1 . A,B = a.e-eq-class (a + b),M and
A11: for A, B being Element of CosetSet M
for a, b being PartFunc of X,REAL st a in A & b in B holds
f2 . A,B = a.e-eq-class (a + b),M ; :: thesis: f1 = f2

now

let A, B be Element of CosetSet M; :: thesis: f1 . A,B = f2 . A,B
A in CosetSet M ;
then consider a1 being PartFunc of X,REAL such that
A12: ( A = a.e-eq-class a1,M & a1 in L1_Functions M ) ;
B in CosetSet M ;
then consider b1 being PartFunc of X,REAL such that
A13: ( B = a.e-eq-class b1,M & b1 in L1_Functions M ) ;
A14: b1 in B by A13, Th38;
A15: a1 in A by A12, Th38;
then f1 . A,B = a.e-eq-class (a1 + b1),M by A10, A14;
hence f1 . A,B = f2 . A,B by A11, A15, A14; :: thesis: verum

end;

hence f1 = f2 by BINOP_1:2; :: thesis: verum