set C = CosetSet (M,k);
defpred S1[ 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 S1[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 S1[z,A,c]
let A be Element of CosetSet (M,k); :: thesis: ex c being Element of CosetSet (M,k) st S1[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 ;
set c = a.e-eq-class_Lp ((z (#) a),M,k);
z (#) a in Lp_Functions (M,k) by ;
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: S1[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 ;
hence c = a.e-eq-class_Lp ((z (#) a1),M,k) by Th42; :: thesis: verum
end;
hence S1[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 S1[z,A,f . (z,A)] from A5: for z being Real
for A being Element of CosetSet (M,k) holds S1[z,A,f . (z,A)]
proof
let z be Real; :: thesis: for A being Element of CosetSet (M,k) holds S1[z,A,f . (z,A)]
let A be Element of CosetSet (M,k); :: thesis: S1[z,A,f . (z,A)]
reconsider z = z as Element of REAL by XREAL_0:def 1;
S1[z,A,f . (z,A)] by A4;
hence S1[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