set C = CosetSet (M,k);
let f1, f2 be Function of [:REAL,(CosetSet (M,k)):],(CosetSet (M,k)); :: thesis: ( ( for z being 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 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
A6: for z being 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
A7: for z being 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 :: thesis: for z being Element of REAL
for A being Element of CosetSet (M,k) holds f1 . (z,A) = f2 . (z,A)

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
A8: ( 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 A6, A8, Th38
.= f2 . (z,A) by A7, A8, Th38 ; :: thesis: verum

end;

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