let f1, f2 be BinOp of (CosetSet M,k); :: 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
f1 . A,B = a.e-eq-class_Lp (a + b),M,k ) & ( 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
f2 . A,B = a.e-eq-class_Lp (a + b),M,k ) implies f1 = f2 )
assume that
A9: 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
f1 . A,B = a.e-eq-class_Lp (a + b),M,k and
A10: 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
f2 . A,B = a.e-eq-class_Lp (a + b),M,k ; :: thesis: f1 = f2

now

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

end;

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