theorem :: VALUED_2:58

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 & ( for x being object st x in dom f holds
f . x is non-empty ) & f [/] c1 = f [/] c2 holds
c1 = c2