set C = CosetSet M;
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;

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 & a in L1_Functions M ) ;
set c = a.e-eq-class (z (#) a),M;
A3: ( z (#) a is PartFunc of X,REAL & z (#) a in L1_Functions M ) by Th01b, A2;
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 A4: a1 in A ; :: thesis: c = a.e-eq-class (z (#) a1),M
then a1 a.e.= a,M by A2, EQC00;
then A5: z (#) a1 a.e.= z (#) a,M by Th08;
( z (#) a1 is PartFunc of X,REAL & z (#) a1 in L1_Functions M ) by Th01b, A4;
hence c = a.e-eq-class (z (#) a1),M by EQC02, A3, A5; :: 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