set C = CCosetSet M;
let f1, f2 be BinOp of (CCosetSet M); :: thesis: ( ( for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
f1 . (A,B) = a.e-Ceq-class ((a + b),M) ) & ( for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
f2 . (A,B) = a.e-Ceq-class ((a + b),M) ) implies f1 = f2 )
assume that
A10: for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
f1 . (A,B) = a.e-Ceq-class ((a + b),M) and
A11: for A, B being Element of CCosetSet M
for a, b being PartFunc of X,COMPLEX st a in A & b in B holds
f2 . (A,B) = a.e-Ceq-class ((a + b),M) ; :: thesis: f1 = f2

now :: thesis: for A, B being Element of CCosetSet M holds f1 . (A,B) = f2 . (A,B)

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

end;

hence f1 = f2 ; :: thesis: verum