set C = CCosetSet M;
let f1, f2 be Function of [:COMPLEX,(CCosetSet M):],(CCosetSet M); ( ( 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)
; f1 = f2
now 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 ;
for A being Element of CCosetSet M holds f1 . (z,A) = f2 . (z,A)let A be
Element of
CCosetSet M;
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
;
verum end;
hence
f1 = f2
; verum