theorem :: VALUED_2:49

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