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) ) ;
A3: ex E being Element of S st
( M . (E `) = 0 & E = dom a & a is_measurable_on E ) by A2, Th35;
set c = a.e-eq-class_Lp ((z (#) a),M,k);
z (#) a in Lp_Functions (M,k) by Th26, 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, A3, Th37, LPSPACE1:32;
hence c = a.e-eq-class_Lp ((z (#) a1),M,k) by Th42; :: 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
A4: 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 A4; :: thesis: verum