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
A7: 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
A8: 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 :: thesis: for A, B being Element of CosetSet (M,k) holds f1 . (A,B) = f2 . (A,B)

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
A9: ( 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
A10: ( B = a.e-eq-class_Lp (b1,M,k) & b1 in Lp_Functions (M,k) ) ;
A11: ( a1 in A & b1 in B ) by A9, A10, Th38;
then f1 . (A,B) = a.e-eq-class_Lp ((a1 + b1),M,k) by A7;
hence f1 . (A,B) = f2 . (A,B) by A8, A11; :: thesis: verum

end;

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