set C = CosetSet (M,k);
defpred S₁[ 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 :: thesis: for z being Element of REAL
for A being Element of CosetSet (M,k) ex c being Element of CosetSet (M,k) st S₁[z,A,c]

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 E -measurable ) 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 :: thesis: for a1 being PartFunc of X,REAL st a1 in A holds
c = a.e-eq-class_Lp ((z (#) a1),M,k)

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);
A5: for z being Real
for A being Element of CosetSet (M,k) holds S₁[z,A,f . (z,A)]

proof

let z be Real; :: thesis: for A being Element of CosetSet (M,k) holds S₁[z,A,f . (z,A)]
let A be Element of CosetSet (M,k); :: thesis: S₁[z,A,f . (z,A)]
reconsider z = z as Element of REAL by XREAL_0:def 1;
S₁[z,A,f . (z,A)] by A4;
hence S₁[z,A,f . (z,A)] ; :: thesis: verum

end;

take f ; :: 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
f . (z,A) = a.e-eq-class_Lp ((z (#) f),M,k)
let z be 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 A5; :: thesis: verum