defpred S₁[ Element of COMPLEX , set , set ] means for f being PartFunc of X,COMPLEX st f in $2 holds
$3 = a.e-Ceq-class (($1 (#) f),M);
set C = CCosetSet M;

A1: now :: thesis: for z being Element of COMPLEX
for A being Element of CCosetSet M ex c being Element of CCosetSet M st S₁[z,A,c]

let z be Element of COMPLEX ; :: thesis: for A being Element of CCosetSet M ex c being Element of CCosetSet M st S₁[z,A,c]
let A be Element of CCosetSet M; :: thesis: ex c being Element of CCosetSet M st S₁[z,A,c]
A in CCosetSet M ;
then consider a being PartFunc of X,COMPLEX such that
A2: A = a.e-Ceq-class (a,M) and
A3: a in L1_CFunctions M ;
set c = a.e-Ceq-class ((z (#) a),M);
A4: z (#) a in L1_CFunctions M by A3, Th18;
then a.e-Ceq-class ((z (#) a),M) in CCosetSet M ;
then reconsider c = a.e-Ceq-class ((z (#) a),M) as Element of CCosetSet M ;
take c = c; :: thesis: S₁[z,A,c]

now :: thesis: for a1 being PartFunc of X,COMPLEX st a1 in A holds
c = a.e-Ceq-class ((z (#) a1),M)

let a1 be PartFunc of X,COMPLEX; :: thesis: ( a1 in A implies c = a.e-Ceq-class ((z (#) a1),M) )
assume A5: a1 in A ; :: thesis: c = a.e-Ceq-class ((z (#) a1),M)
then a1 a.e.cpfunc= a,M by A2, A3, Th30;
then A6: z (#) a1 a.e.cpfunc= z (#) a,M by Th26;
z (#) a1 in L1_CFunctions M by A5, Th18;
hence c = a.e-Ceq-class ((z (#) a1),M) by A4, A6, Th32; :: thesis: verum

end;

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

end;

consider f being Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M) such that
A7: for z being Element of COMPLEX
for A being Element of CCosetSet M holds S₁[z,A,f . (z,A)] from BINOP_1:sch 3(A1);
take f ; :: thesis: for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
f . (z,A) = a.e-Ceq-class ((z (#) f),M)
let z be Complex; :: thesis: for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
f . (z,A) = a.e-Ceq-class ((z (#) f),M)
let A be Element of CCosetSet M; :: thesis: for f being PartFunc of X,COMPLEX st f in A holds
f . (z,A) = a.e-Ceq-class ((z (#) f),M)
let a be PartFunc of X,COMPLEX; :: thesis: ( a in A implies f . (z,A) = a.e-Ceq-class ((z (#) a),M) )
z in COMPLEX by XCMPLX_0:def 2;
hence ( a in A implies f . (z,A) = a.e-Ceq-class ((z (#) a),M) ) by A7; :: thesis: verum