theorem :: VALUED_2:46

for X being set
for Y being complex-functions-membered set
for c1, c2 being Complex
for f being PartFunc of X,Y st f <> {} & f is non-empty & f [+] c1 = f [+] c2 holds
c1 = c2