set C = CosetSet M,k;
defpred S₁[ Element of REAL , set , set ] means for f being PartFunc of X,REAL st f in $2 holds
$3 = a.e-eq-class_Lp ($1 (#) f),M,k;

A1: now

let z be Element of REAL ; :: thesis: for A being Element of CosetSet M,k ex c being Element of CosetSet M,k st S₁[z,A,c]
let A be Element of CosetSet M,k; :: thesis: ex c being Element of CosetSet M,k st S₁[z,A,c]
A in CosetSet M,k ;
then consider a being PartFunc of X,REAL such that
A2: ( A = a.e-eq-class_Lp a,M,k & a in Lp_Functions M,k ) ;
B2: ex E being Element of S st
( M . (E ` ) = 0 & E = dom a & a is_measurable_on E ) by A2, EQC00a;
set c = a.e-eq-class_Lp (z (#) a),M,k;
z (#) a in Lp_Functions M,k by Th01bLp, A2;
then a.e-eq-class_Lp (z (#) a),M,k in CosetSet M,k ;
then reconsider c = a.e-eq-class_Lp (z (#) a),M,k as Element of CosetSet M,k ;
take c = c; :: thesis: S₁[z,A,c]

now

let a1 be PartFunc of X,REAL ; :: thesis: ( a1 in A implies c = a.e-eq-class_Lp (z (#) a1),M,k )
assume a1 in A ; :: thesis: c = a.e-eq-class_Lp (z (#) a1),M,k
then z (#) a1 a.e.= z (#) a,M by A2, B2, EQC00c, LPSPACE1:32;
hence c = a.e-eq-class_Lp (z (#) a1),M,k by EQC02bx; :: thesis: verum

end;

hence S₁[z,A,c] ; :: thesis: verum

end;

consider f being Function of [:REAL ,(CosetSet M,k):],(CosetSet M,k) such that
A7: for z being Element of REAL
for A being Element of CosetSet M,k holds S₁[z,A,f . z,A] from BINOP_1:sch 3(A1);
take f ; :: 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
f . z,A = a.e-eq-class_Lp (z (#) f),M,k
let z be Element of REAL ; :: thesis: for A being Element of CosetSet M,k
for f being PartFunc of X,REAL st f in A holds
f . z,A = a.e-eq-class_Lp (z (#) f),M,k
let A be Element of CosetSet M,k; :: thesis: for f being PartFunc of X,REAL st f in A holds
f . z,A = a.e-eq-class_Lp (z (#) f),M,k
let a be PartFunc of X,REAL ; :: thesis: ( a in A implies f . z,A = a.e-eq-class_Lp (z (#) a),M,k )
assume a in A ; :: thesis: f . z,A = a.e-eq-class_Lp (z (#) a),M,k
hence f . z,A = a.e-eq-class_Lp (z (#) a),M,k by A7; :: thesis: verum