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

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

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

proof

let z be Real; :: thesis: for A being Element of CosetSet M holds S₁[z,A,f . (z,A)]
let A be Element of CosetSet M; :: 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 A7;
hence S₁[z,A,f . (z,A)] ; :: thesis: verum

end;

take f ; :: thesis: for z being 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 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 A8; :: thesis: verum