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 ($1 (#) f),M;
set C = CosetSet M;

A1: now

let z be Element of REAL ; :: thesis: for A being Element of CosetSet M ex c being Element of CosetSet M st S₁[z,A,c]
let A be Element of CosetSet M; :: thesis: ex c being Element of CosetSet M st S₁[z,A,c]
A in CosetSet M ;
then consider a being PartFunc of X,REAL such that
A2: A = a.e-eq-class a,M and
A3: a in L1_Functions M ;
set c = a.e-eq-class (z (#) a),M;
A4: z (#) a in L1_Functions M by A3, Th24;
then a.e-eq-class (z (#) a),M in CosetSet M ;
then reconsider c = a.e-eq-class (z (#) a),M as Element of CosetSet M ;
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 (z (#) a1),M )
assume A5: a1 in A ; :: thesis: c = a.e-eq-class (z (#) a1),M
then a1 a.e.= a,M by A2, A3, Th37;
then A6: z (#) a1 a.e.= z (#) a,M by Th32;
z (#) a1 in L1_Functions M by A5, Th24;
hence c = a.e-eq-class (z (#) a1),M by A4, A6, Th39; :: thesis: verum

end;

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

end;

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