set C = CosetSet M,k;
let f1, f2 be Function of [:REAL ,(CosetSet M,k):],(CosetSet M,k); :: thesis: ( ( for z being Element of REAL
for A being Element of CosetSet M,k
for f being PartFunc of X,REAL st f in A holds
f1 . z,A = a.e-eq-class_Lp (z (#) f),M,k ) & ( for z being Element of REAL
for A being Element of CosetSet M,k
for f being PartFunc of X,REAL st f in A holds
f2 . z,A = a.e-eq-class_Lp (z (#) f),M,k ) implies f1 = f2 )
assume that
A8: for z being Element of REAL
for A being Element of CosetSet M,k
for a being PartFunc of X,REAL st a in A holds
f1 . z,A = a.e-eq-class_Lp (z (#) a),M,k and
A9: for z being Element of REAL
for A being Element of CosetSet M,k
for a being PartFunc of X,REAL st a in A holds
f2 . z,A = a.e-eq-class_Lp (z (#) a),M,k ; :: thesis: f1 = f2

now

let z be Element of REAL ; :: thesis: for A being Element of CosetSet M,k holds f1 . z,A = f2 . z,A
let A be Element of CosetSet M,k; :: thesis: f1 . z,A = f2 . z,A
A in CosetSet M,k ;
then consider a1 being PartFunc of X,REAL such that
A10: ( A = a.e-eq-class_Lp a1,M,k & a1 in Lp_Functions M,k ) ;
thus f1 . z,A = a.e-eq-class_Lp (z (#) a1),M,k by A8, A10, EQC01
.= f2 . z,A by A9, A10, EQC01 ; :: thesis: verum

end;

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