set C = CCosetSet M;
let f1, f2 be Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M); :: thesis: ( ( for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
f1 . (z,A) = a.e-Ceq-class ((z (#) f),M) ) & ( for z being Complex
for A being Element of CCosetSet M
for f being PartFunc of X,COMPLEX st f in A holds
f2 . (z,A) = a.e-Ceq-class ((z (#) f),M) ) implies f1 = f2 )
assume that
A8: for z being Complex
for A being Element of CCosetSet M
for a being PartFunc of X,COMPLEX st a in A holds
f1 . (z,A) = a.e-Ceq-class ((z (#) a),M) and
A9: for z being Complex
for A being Element of CCosetSet M
for a being PartFunc of X,COMPLEX st a in A holds
f2 . (z,A) = a.e-Ceq-class ((z (#) a),M) ; :: thesis: f1 = f2

now :: thesis: for z being Element of COMPLEX
for A being Element of CCosetSet M holds f1 . (z,A) = f2 . (z,A)

let z be Element of COMPLEX ; :: thesis: for A being Element of CCosetSet M holds f1 . (z,A) = f2 . (z,A)
let A be Element of CCosetSet M; :: thesis: f1 . (z,A) = f2 . (z,A)
A in CCosetSet M ;
then consider a1 being PartFunc of X,COMPLEX such that
A10: ( A = a.e-Ceq-class (a1,M) & a1 in L1_CFunctions M ) ;
thus f1 . (z,A) = a.e-Ceq-class ((z (#) a1),M) by A8, A10, Th31
.= f2 . (z,A) by A9, A10, Th31 ; :: thesis: verum

end;

hence f1 = f2 ; :: thesis: verum